Repository navigation
feat(WordRAM): recover witnesses for native ET record products - #1661
Merged
SamuelSchlesinger merged 130 commits intoOct 30, 2026
Merged
Conversation
Adapt the finite counting interface and signed digit expansion from anthropics/formal-math@16a5ce4 for milestone #1438. This is a mathematical interface; native preprocessing, fast solvers and full composition remain under #1394.
Adapt the complete finite Theorem 17 splitting and recovery component, using the existing three weight matrices, lopsided graphs, modular counts and EqOn answer interface. Prove exact integer/real capacity bridges so the finite constructions and scans are computable. Preserve Anthropic source credit; keep the native 3SUM endpoint open in #1394. Validation: all six gates in scripts/check.sh pass, with LEAN_NUM_THREADS=1 and cache downloads disabled after bootstrap. Full hygiene, changed-source check-simp, changed-file lints and git diff --check pass. Curated abstracts and rendering are unaffected. AI-assisted implementation/self-review by Codex worker codex-three-sum-splitting-t3-0a4d90c0; independent review will be recorded in the PR.
Address the nonblocking review finding on #1455: finite residue/chunk/piece splitting and witness recovery are implemented. Preserve native preprocessing, fast solvers, full input/time/width composition and exponent 1.9992 as open work under #1394. Documentation only. Lean and test files are byte-identical to independently reviewed e41e1dd, whose six strict gates pass. Checked the diff, milestone reference, implementation paths, hygiene and changed-file lints. Abstracts and rendering are unaffected.
Implement fixed native residue, histogram and composed collision-counting programs with explicit frames, local word-fit contracts, exact mathematical collision semantics and charged bound 34n + 5M + 18 (halt excluded). Implementation layer for #1454 under #1446/#1394, not full preprocessing. Sorting/frontend, prime searches, heavy extraction, recursion/output and global logarithmic-width/subquadratic-time composition remain open. Curated abstracts: no impact on headline statements, definitions or scope. Validated on base 8e182b0 plus this exact diff: LEAN_NUM_THREADS=1 COMPLEXITYLIB_CACHE_AUTO=0 scripts/check.sh: all six gates passed, including strict test/global axiom audit. Changed-file lints against that base, hygiene --check-simp and git diff --check passed. Final run followed resolution of shared-host disk/memory pressure; failed earlier attempts are not counted as validation. Independent read-only agent correctness/API review by /root/review_native_histogram approved the final source blobs after replacing three private clear helpers with WordRAM.clear. No remaining blockers; optional Count parameter-frame API can accompany its minimum-search client. This is within-fleet agent review, not outside-coordinator or human approval. Outside coordinator review is required before integration. AI assistance: OpenAI Codex implementation/self-review and a separate Codex review context. Native programs/counting proofs are original; existing Anthropic mathematical source credit is preserved unchanged.
Implement the complete finite mathematical milestone of #1463 above #1464: valid layouts, batch-product correctness/error exclusion, arbitrary-N tiling, exact requested signed products, order/cardinality estimates, geometric tails and the derived sparse bounds. At D=4^m, L=19m, D^18<=N and |W|*2^m<=N^2, encoding entries are bounded by4*N^2/D^(1/18), contributing leaves by33 and passed-set cardinalities by(19m+1)*33 times that scale. Add finite magnitude and auxiliary object-count bounds. None are native instruction costs. All six final local gates pass: strict build, aggregate check, strict tests, environment lint, style lint and init-import check. Hygiene --check-simp, changed-file lints (14 library modules,1 new test) and diff --check pass. Tests kernel-check signed results3,20,0,-8, true padding, empty/sparse and negative-order boundaries, and instantiate all aggregate bounds with jointly satisfiable m=1 parameters and symbolic matrices without resource overrides. Read-only math/API review by /root/thin_product_review is clear after fixed doc references/magnitude wording/quotation hygiene. Focused final delta review by /root/thin_product_final_delta_review is clear for tree b021e2d, reusing the prior mathematics review. These are internal agent reviews, not outside coordinator or human approval. Source: anthropics/formal-math@16a5ce4, selective Section2 finite mathematics; Anthropic credit/NOTICE retained. Abstract assessment: no impact on selected headlines, catalogue or rendering. Full native tensor/sparse-product/Exact Triangle code, native Chan-He #1446, whole input/time/width composition and improved1.9992 remain under #1394. AI assistance: implementation and reviews with OpenAI Codex, worker session codex-thin-product-math-20261028.
Implement fixed 24-register parameter code with charged numeric helpers, exact existing Chan–He outputs, preserved input memory, derived logarithmic width and subquadratic native time. Add executed boundary and input-init contract examples. Original implementation and proofs credited to Erik Demaine; AI assistance by OpenAI Codex. Part of #1446; independent complete parameter subtask #1458.
Restack #1463 above repaired #1464 without changing the reviewed mathematics. Rewrite 149 documentation blocks in 14 modules as standalone descriptions; replace operation-cost and word-size narratives with the exact entry, leaf, passed-set and specified-value quantities proved. Preserve pinned Anthropic credit, source locators, statements, definitions, proof bodies and imports. An independent comparison with original ee288fb confirms that all code bytes outside comments are identical, including code whitespace. Validation of this final tree: all six gates pass together (strict build, aggregate check, strict tests, environment lint, style lint, init imports). Citation-aware full hygiene --check-simp, changed-file lints (14 library modules, one test) and git diff --check pass. Lean MCP FiniteMagnitude diagnostics finish without errors or warnings. Serial Smoke/Axioms warmups avoid the shared-host memory failure previously seen when these import-heavy clients run together. Tests and substantive math/API review evidence are retained from the original reviewed tree b021e2d in ee288fb. This change is documentation-only; /root/draft_thin_docs authored the scratch map and the continuation worker inspected/applied it. That drafting is not independent review. Earlier math reviews are inside-fleet agent reviews, not outside or human approval. Outside coordinator review will be requested on the final PR. No selected abstract, catalogue or rendering is affected. PR publication remains held while native dependent restacks are repaired, per root sequencing. #1394 remains open: native shared encodings/pruning/Exact Triangle, Chan-He #1446, complete Convolution/ordinary input/time/width composition and the improved Section4 route to exponent1.9992 are not supplied by these finite counts. AI assistance: OpenAI Codex workers codex-thin-product-math-20261028, codex-three-sum-continuation-t3-3dda8289 and /root/draft_thin_docs.
Complete the shared left/right encoder milestone #1493 above parent b4936ce (#1496). Fixed standard-WordRAM code with 32 registers computes every public encodingL/encodingR leaf from actual initialized flat signed inputs. The native bound is 240*(L+1)*10^L instructions plus halt, with explicit magnitude/address inequalities, two alternating buffers, charged initialization/copying and the complete outside frame. The full ordinary native 3SUM objective #1394 remains open; this component supplies no sparse-query or Exact Triangle solver. Validation of tree b598513 against b4936ce: all six gates pass together (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports), full citation-aware hygiene --check-simp, changed-file lints (13 library modules, one new test) and diff checks pass. Tests execute both encoders at depths zero, one and two, compare all 100 depth-two leaves with the unchanged public encodings, preserve input/frame sentinels, and cover adjacent word widths and all three copy block orders. Kernel-checked concrete flat executions discharge every width/magnitude premise. Selected abstracts, catalogue and rendering are unaffected. AI assistance: OpenAI Codex implementation and self-review by delegated worker codex-shared-encoding-t3-03b600bd. Independent correctness/API review is pending; this is not an approval or a claim that the complete 3SUM objective is done.
Connect the zero-depth and two-stage regression memory witnesses to the actual prefix Runs already proved by runs_left, rather than discarding that conjunct. Bound the prefixes by 240 and 72000 instructions and expose the same executions' charged halt at n+1. All library code is unchanged from ad3e097 (tree b598513). Validation of tree 8277017 against actual parent b4936ce: all six gates pass together (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports), full citation-aware hygiene --check-simp, fresh changed-file lints (13 library modules, one test), strict PR-draft declaration-name check and staged/unstaged diff checks pass. Independent nonauthor agent review 8034f3da approved exact ad3e097/tree b598513, covering full code/model/cost/width/source and ArrayCopy with no blockers. It is inside-fleet review, not outside approval. This test-only delta addresses its optional witness-connection finding; focused final test/source-mapping review remains pending through the parent coordinator. No selected abstract, catalogue or rendering impact. The full ordinary native 3SUM objective #1394 remains open; this implements encoder issue #1493. AI assistance: OpenAI Codex implementation/self-review by delegated worker codex-shared-encoding-t3-03b600bd. Publication remains on hold for focused review; this commit is not approval or a whole-3SUM completion claim.
Work in progress for #1526. Fixed native controller and initialized-input interpreter regressions, numerical child-set bridge, call-count potential, charged power/scan/clear/frame/arithmetic/return kernels. Individual current Lean modules have clean MCP diagnostics; the earlier strict targeted scan/count/value/test checkpoint passed. The complete global controller invariant, native evaluator theorem, actual initialized flat-run clients and sparse charged bound remain unfinished. No full six-gate or independent review claim; no PR submission. Full #1394 endpoint remains open. AI-assisted implementation by codex-three-sum-continuation-t3-3dda8289.
Address the bounded nonblocking review findings on #1496. Keep Nat.choose_le_exp_mul_div_pow unchanged while deriving it from Cslib.sum_choose_le_exp_one_mul_div_pow in the existing real binomial module; remove the redundant module and migrate its import. Preserve Anthropic, Samuel Schlesinger, OpenAI and Erik Demaine credit. Kernel-check an actual mixed inner/outer L2,m1 signed pruned result of -8, remove two signature-only tests and retain positive admitted-parameter checks. Paraphrase the identified source-derived sentence, shorten generic source boilerplate and record the generic naming follow-up. No public mathematical statement or definition changes meaning; no selected abstract or endpoint promotion. Final validation/source/review evidence is in PR #1496. AI-assisted implementation by codex-three-sum-continuation-t3-3dda8289.
Implement the complete bounded #1523 native component under #1394. A fixed 96-register standard WordRAM program computes valid subset/inverse tables and a deterministic existing Layout, prepares all padded signed row/column bands, calls the unchanged #1520 encoders once per shared band, collects every leaf, and restores the entire initialized input prefix and outside frame. The State.init and flat Runs/Executes clients bind the actual output memory to public encodingL/R in the unchanged leafIndex order (P0 digit 9). All powers, mask/popcount/root/table loops, indices, guarded matrix addresses, initialization, copying, encoder calls, loop controls and halt are charged. The generic bound is 4096*(L+1)*(1+N*4^m+2^L+2*numBands*10^L), plus halt; at L=19m and N>=(4^m)^18, the full charged run is <=81920*(L+1)*N^2/(4^m)^(1/18). Width assumptions are explicit original-parameter inequalities: the wordBudget fits target w+2 and 7^L*A < 2^(w-1), w>0, A>=0. Actual signed kernels use at most 15/17 instructions for add/subtract, already included through the unchanged encoder's real cost. No all-state fit, callback, solver, assumed run/cost or source machine semantics is a hypothesis. Symbolic positive-depth thin native examples and concrete signed/padded/frame/width-boundary executions establish nonvacuity. Pinned source: anthropics/formal-math@16a5ce4, 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/AllBands.lean:230-239,262-271 and BandArrayFacts.lean:107-113. Verified checkout files equal their pinned Git blobs and all PR-draft quotations match those exact line slices. The source's row/column encoding predicates map to runs' quantified original matrices, all bands and all leaves on computed MaskTable.layout; Light limits/program maps, callee contracts and source time hypotheses are replaced by actual native code proofs, not imported. The block index is beta*K0+(side? h:g), and row is block*N0 plus the compressed outer offset. Shared tile pointers and retained table words are exposed by tileInputBases/tile_input_values/table_word_layout. Reuse unchanged WordRAM control/rename/copy/signed APIs, Layout/bandArray/encoding mathematics and Mathlib finite index/sorted-set APIs. New mask scans, dense inverse lookup, direct base-seven decoder and native execution/cost composition are original. Small native-power/ordered-filter/positional-digit/row-major lemmas live in narrow topic modules. Retain Anthropic, PBC source credit and NOTICE. Validation: PASS all six strict gates (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports), serial Smoke/Axioms warmups and the global Axioms audit; full citation-aware hygiene --check-simp, fresh actual-base changed-file lints, strict PR-name and diff checks. Validated with LEAN_NUM_THREADS=1 and cache downloads disabled. Windows static metadata reads used PYTHONUTF8=1; no Lean/source change was needed. New Lean files use ordinary non-executable file modes. Exact payload tree bdfc5a1. Targeted Lean MCP endpoint/tests and pinned quote identity also pass. No PR has been opened; independent exact-revision correctness/API/source-mapping review is pending. Abstract assessment: no impact on selected abstracts, models or scope; no new headline or PDFs. Pruned queries, products, solvers and whole ordinary 3SUM remain open under #1394. Base #1520 remains unchanged at 3b9234d. AI assistance: Codex implementation/proofs, session codex-native-bandprep-t3-03b600bd, under delegating-worker coordination. Existing unchanged encoder outside-review evidence is PR1520#issuecomment-6477077023; final new-component review pending.
…tions Work in progress for #1526, not a submitted component. Complete native parent accumulation loop (31N+3), internal sparse initialization (7N+8), computed child push (15), shared actual frame-word store, executable query-code inverse/requested-set bridge and recursive timestamp allowance. These current modules have clean targeted Lean MCP diagnostics; actual interpreter and kernel digit/request regressions pass. Changed-scope hygiene --check-simp and diff check pass. The general node/controller continuation proof, actual initialized full evaluator theorem and final sparse charged bound remain unfinished; no full six-gate or independent review claim. AI-assisted implementation by codex-three-sum-continuation-t3-3dda8289; full #1394 remains open. Final current-tree checkpoint: strict build --wfail --iofail of Accumulate, Clear, Push, Frame, Powers, Leaf, Weight, Scan and SchonhagePruned tests passed together (3596 jobs); scope hygiene --check-simp and diff checks pass. This is a partial implementation checkpoint, not an all-six-validated PR or completed #1526 milestone.
WIP #1526. Factor root scan setup and root finish; prove the actual eleven-instruction root-frame initialization and exact memory/register frame. Current Root MCP diagnostics clean. Full node/controller composition remains unfinished; no PR or full-six claim. AI-assisted continuation by codex-three-sum-continuation-t3-3dda8289.
Address the sole P2 finding from the independent #1523 review of cb261f6: remove duplicate Nat.ofDigits_ofFn and publicly import the existing radix module. The finite-function numbering bridge uses Nat.ofDigits_ofFn_eq_sum. Its statement is unchanged. Existing radix declarations, proofs and source credit are unchanged; no native program, endpoint statement or test changed. Validation on exact final tree 4807cb9: PASS all six strict gates together (build --wfail --iofail, mk_all --check, test --wfail --iofail including global Axioms, lint, lint-style, checkInitImports), fresh actual-base changed-module lints (29 library/1 test), full citation-aware hygiene --check-simp, strict draft-name and diff checks. Serial LEAN_NUM_THREADS=1; optional cache downloads disabled. Lean MCP also reports clean diagnostics for the changed bridge. Logs are in .lake/codex-three-sum-continuation/band-review-six in the continuation checkout. Original native implementation and all full correctness/API/source-mapping review coverage retained. Review record: #1523 (comment) Original implementation/validation handoff: #1523 (comment) Focused final delta review pending before PR publication. No impact on selected abstracts, models or scope; no new headline. Complete #1394 native 1.9992 endpoint remains open. AI assistance: bounded reuse fix and validation by Codex session codex-three-sum-continuation-t3-3dda8289. Original author credit remains on cb261f6.
Continue #1526 implementation under #1394; this is explicitly partial WIP, not a complete component or PR submission. Full recursive node composition, initialized input/flat clients, derived global fits and total-time theorem remain open. No solver or all-state fit/execution/time certificate is assumed. Check full root setup/scan/frame (20Q+19), report (9Q+3), leaf/return (24), loaded leaf step (43), internal entry (7N+28), native nonempty child scan/push (20N+42), empty-child scan/advance (20N+33), returned-child accumulation (31N+29), and final return (26) against the actual standard fixed native Code. KernelRegs describes only constant/pointer register values. Node footprints preserve the ancestor rows. The zero-depth node matches existing Pruned.result and the finite traceWeight; its continuation uses the existing ExecWithin.loop_iter. No alternative machine or run semantics is introduced. The reporting-body/controller names are definitionally identical Code trees. ScanMemory.congr transports the existing representation across disjoint writes and removes duplicate root proof plumbing; push exposes its four-store frame. Validation: targeted Lean MCP diagnostics clean for every new/updated phase and ComplexityTests/SchonhagePruned.lean. Native interpreter regressions retain depths 0/1/2, both signs, repeated/empty/mixed queries and an outside sentinel. New kernel examples discharge the general node/register/address/signed premises, connect the same negative-product final memory to charged controller execution, and prove an empty leaf preserves the prior value cell. Diff whitespace passes. No aggregate/all-six validation claimed: root/native audit coordination hold is respected. Exact partial checkpoint tree 7fa4da6. Abstracts: no impact; no new headline or endpoint claim. Original 1.9992 objective and sparse-product/ET/final composition remain open under #1394. AI assistance: Codex implementation/proofs by continuation worker codex-three-sum-continuation-t3-3dda8289.
Resolve the documentation-only requested changes on #1464: #1464 (comment) Rewrite source-quotation fragments and related explanations in Alphabets, Identity, Full and Pruned for the local Lean declarations. Preserve the mathematical attribution, bibliography keys, source pin and copyright. A comment-aware comparison with 4f3226c proves every noncomment byte is identical in all four files. No declaration, proof, definition, program, import or test changes. Existing checked source-statement quotations and notation/quantifier/model/resource mapping in the PR remain unchanged. The final source-comment screen compares against quoted fragments in the actual pinned Sec2 and Statements/PaperStatements files, including the known local renames; no substantial quoted fragment remains unmarked. Validation is recorded for this exact tree in PR #1464. Source checkpoint tree 8c3b87b. No abstract/catalogue/model/scope or rendering impact; no new headline. The full native 1.9992 endpoint remains open under #1394. Ancestor and descendant remotes are unchanged. AI assistance: documentation repair and validation by Codex continuation worker codex-three-sum-continuation-t3-3dda8289. Existing independent mathematical/API and checked-source review coverage is retained; outside review of the bounded documentation delta is requested, with no new review agent commissioned.
Finish bounded #1545 from exact #1536 head66036150a. Replace generic level/inner/outer API vocabulary with order-embedding/subset/complement names. Remove five redundant membership/range/congruence wrappers, using Mathlib's orderEmbOfFin_mem/range_orderEmbOfFin and ordinary substitution directly. Migrate every actual Levels/Batch proof client with no deprecated aliases. Keep filter_glue's generic name and rename its predicate parameter to P. The retained generic statement headers are identical after the documented renaming and binder alpha-renaming. All 48 Levels and 13 Batch declaration statements and all definition bodies remain unchanged. The entire native Encoding module is token-identical after comment removal; every other native library file is unchanged. Source credit and pin are retained. Thus existing State.init, Signed.encode, width/frame/cost and encodingL/R meanings remain. Put the sum/option-versus-flat-digit explanation at the actual leftDigits, rightDigits and termDigits hover docs, preserving their enumeration bodies and order (row-major P terms, P0 digit9). Update the UPSTREAM naming follow-up. Add generic nonconsecutive signed/zero/Option reconstruction clients using Mathlib's orderEmbOfFin_unique, plus the routed optional #1536 asymmetric native L4,m1,N29 prefix tests. Those compute headers/count/tables/snapshot and decode/read ranks1 and2 with K0=2, distinguishing quotient/remainder blocks and signed values without a full10^4-leaf encoder run or native body edits. Reuse unchanged outside coverage: PR1496#issuecomment-6477111644 atb4936ce28, PR1496#issuecomment-6480746578 at68bbe40e3, and PR1536#issuecomment-6480852097 at66036150a12046b29986d8f108c0afaf49d01c61. These are agent reviews, not human approval. No new cited mathematical result or machine model is introduced. Validation: PASS build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style and checkInitImports, with serial Smoke/global Axioms warmups. Full citation-aware hygiene --check-simp, fresh changed-file lints against actual base66036150a, strict PR-name and diff checks, and source/native identity checks PASS. One thread, no cache downloads, PYTHONUTF8=1 on Windows. Targeted MCP checks, full hygiene --check-simp and source/native identity checks pass. Final source tree: 0c21b60. No source/ancestor merges or restacks. Abstract assessment: no impact; no selected theorem/model/meaning/scope or PDF change. This is generic ergonomics/testing only; full #1394 remains open. AI-assisted implementation by codex-native-bandprep-t3-03b600bd, under parent continuation-worker coordination. No new review agent commissioned; ordinary outside coordinator review is requested when the bounded PR is ready.
WIP checkpoint for #1526; no PR and no completed component claim. The actual fixed native controller now has a depth-inductive execution proof with original Pruned.result values, stored queries/frames, concrete spatial preservation, input-derived signed fits and traceWeight charged continuation. Root loop exit discharges the continuation. All new library modules through Recursive.exec_ready have clean targeted Lean MCP diagnostics. New concrete entry/result client reports no diagnostics, but the complete existing test file is still elaborating its VM regression commands; no final test-pass or all-six claim. Initialization/root-list/report/flat State.init composition, global width/fit clients, full component validation and independent review remain open. Aggregate checks are held for the coordinated root validation slot. GenericRAM/Signed/Fits.lean is the unchanged blob from independently owned PR #1552, commit f276db1; credit retained. No native program body changed in this checkpoint. All proofs and invariant definitions are original native work; existing mathematical pruning/encodings retain their source credit. No selected-abstract impact or whole-3SUM endpoint claim. AI-assisted implementation by codex-three-sum-continuation-t3-3dda8289.
Advance CSLib to 8a8ad748 and synchronize Mathlib, the documentation generator, Verso, and all three lockfiles with Lean v4.36.0-rc2. Keep the root and documentation projects on the same inherited dependency revisions.
Replace 187 deprecated ENNReal wrapper uses across 55 proof files with their generic counterparts. The exact mapping is: - ENNReal.tsum_le_tsum -> tsum_le_tsum (94) - ENNReal.tsum_add -> tsum_add (54) - ENNReal.tsum_eq_zero -> tsum_eq_zero_iff (14) - ENNReal.summable -> CompleteLattice.summable (6) - ENNReal.tsum_comm -> tsum_comm (6) - ENNReal.tsum_prod' -> tsum_prod' (5) - ENNReal.le_tsum -> le_tsum (5) - ENNReal.tsum_eq_add_tsum_ite -> tsum_eq_add_tsum_ite (2) - ENNReal.tsum_sigma -> tsum_sigma (1) The old wrappers invoke these same theorems specialized to ENNReal. All five le_tsum calls already pass the function by name. No statements or definitions change.
Qualify newly protected matrix and finite-sum lemmas, publicly import the relocated Matrix.Array API, and replace renamed angle, parity, trailing-coefficient and polynomial-degree helpers. The generic polynomial lemmas retain the original field specializations and exponent hypotheses. No theorem statement or definition body changes. Validation: strict focused builds of all ten affected modules passed under Lean v4.36.0-rc2. Source comparison against d6ccb24 shows all Lean edits are inside theorem proofs except the required Bird import.
Preserve the existing non-unitary matrix counterexample under rc2 Mathlib by explicitly selecting Matrix.mul_apply, as in the library proof repairs.
Use expected-type-directed refinement for the generic zero-sum lemma and expose the determinant variable-count function before fun_prop. Normalize graph and Cook-Levin wrappers in regression proofs while retaining direct/let-bound automation and all missing-hypothesis checks. Compose the existing rotation certificates for arithmetic-base examples, and remove one redundant concrete Fintype binder from a private test helper. Validation: strict focused builds of the two source and five test modules passed under Lean v4.36.0-rc2. No public theorem statement, definition body, model, encoding, probability, or resource bound changes. No heartbeat or fun_prop compatibility option was introduced.
Complete #1639 candidate on pinned main d6ccb24. Preserve source checkpoint b461744 and its normal merge c02ed27. Final validated source tree: 78662a0. No later main snapshot was merged. One fixed 400-register standard-native program executes original State.init input, real preparation, first-record selection, actual queried product and original signed weight verification. Generic execution covers any occupied record. Same-y prefix Runs, charged halt, exact selected chunk/piece correctness, original coordinates, full frame and S <= falsePositiveCount + actual returned flag are proved. Width admission is positive logarithmic for polynomial original scalars/weights; prefix words/support are polynomial independently of every wider admitted physical width. Code has <=133120 flat slots including halt and does not read word width. Outer ET/prime/global choices, aggregate saving and ordinary 3SUM 1.9992 remain open under #1394. All six gates PASS on the exact final tree, LEAN_NUM_THREADS=4, cache downloads disabled: lake --no-cache build --wfail --iofail : exit 0 (608.22 s) lake --no-cache exe mk_all --check : exit 0 (8.61 s) lake --no-cache test --wfail --iofail : exit 0 (845.36 s) lake --no-cache lint : exit 0 (52.05 s) lake --no-cache exe lint-style : exit 0 (15.28 s) lake --no-cache exe checkInitImports : exit 0 (17.28 s) Gates 1-2 retained across provider/agent cancellation; unfinished gates 3-6 resumed only after native PID/command-line checks proved the prior runner had ended. Same source and flags throughout; interrupted partial tests are archived and not counted as passed. Strict tests explicitly built WordRAMExactTriangleWitnessScan, QueryValues, RecordWitness, Smoke and global Axioms. Cases cover signed success/failure, empty intervals, actual producer pair order, valid-geometry post-product consumer short circuit/false positives, frame sentinels and a fully admitted symbolic initialized positive-depth pipeline. VM consumer fixtures are not represented as full producer/product VM executions. Final static checks PASS: full hygiene --check-simp; fresh exact-base 32-library and 3-test module lints; changed-file/doc/test checks; strict body names; complete base, staged and unstaged diff --check; actual source-pin/Git-blob/quote mapping. Eight final Lean MCP targeted umbrella/client diagnostics were clean before the final sequence. Compatibility preserves own b461 mathematical/native bodies, statements, attributes and imports. Canonical root imports and four source-reference doc tokens are fixed. Only CRLF -> LF changes in five Lean files and two docs resolve the caught whitespace failure; all non-EOL bytes are identical. All 3876 other protected pinned-main source, abstract and test files are unchanged. Original credit and all landed main prose remain. No curated abstract/catalogue/rendering impact. No source/API/model change was hidden as compatibility. New whole-layer APIs/proofs still require fresh nonauthoring review. Pinned source: anthropics/formal-math@16a5ce4, Programs/Sec3/Theorem17/Witnesses/Scan.lean:73-89, ScanPairs.lean:69-70 and finite Sec3/Theorem17/Witnesses.lean. Actual read-only source bytes equal pinned Git blobs. Checked quote: execsUpto acc hit f w + f.toNat ≤ failsUpto acc hit w + (foundAt acc hit f w).toNat Light semantics/costs are not imported or assumed. Native code/ABI/constants are proved directly. Source incoming flag may be arbitrary; this header begins false. Finite scan returns first zero, native verifier last zero: failure equivalence is proved, not an exact witness-order identity. Source credit retained. Evidence: .lake/codex-three-sum-continuation/record-witness/final-validation/ summary.json, static-summary.json, test-coverage.json, source-identity.json, source-mapping.json, eol-normalization.json and per-command logs. Earlier interrupted CRLF/bootstrap/syntax/cancellation records are retained separately. This commit is the durable public validation record; #1639 links it. Fresh whole-layer review pending. AI assistance: Codex implementation/proofs, Lean MCP and scripted validation.
Collaborator
Author
|
Independent non-authoring agent Read the native verifier/controller and proof chains, actual initialized product→consumer composition, query/chunk readback, detection and finite failure injection, API migrations and pinned sources. Original signed-weight verification is exact; the last-zero native witness is related to the finite first-zero scan through their failure conditions. Actual scans satisfy Reviewed source mapping and seven EOL-only normalizations. Validation relies on the recorded exact-tree six-gate/static evidence, including the three new suites, Smoke and Axioms; the reviewer ran no build. Approval covers per-record recovery. Global prime/parameter choices, the outer ET loop, aggregate saving and #1394/1.9992 remain open. |
This was referenced Oct 29, 2026
…ib-rc2-sync-1648-codex
SamuelSchlesinger
approved these changes
Oct 29, 2026
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
Collaborator
There was a problem hiding this comment.
Coordinator codex-coord-20261029-1732 — APPROVE this source revision, with outside-author-fleet agent review by /root/review_native_record_1661 and its non-authoring bounds_width subreviewer. This is agent review, not human approval.
The actual signed verifier and short-circuit controller compose with the real producer/product and retain original weights, query rank/nonrepetition and caller frames. Product detection plus distinct failed queries justifies S ≤ falsePositiveCount + returnedFlag. We checked the same-state initialized prefix/halt/witness conclusions, halt-inclusive resource accounting, logarithmic admission and width-independent prefix/support bounds, and the fully admitted positive-depth success client. Consumer VM fixtures are separately identified as post-product fixtures. The pinned Scan/ScanPairs source mapping and quoted locator were checked directly. API placement and migrated preparation clients are appropriate; no abstract impact.
This approves per-record recovery only. Global prime/parameter choice, the outer loop, aggregate ET savings and #1394 remain open. No local elaboration/build was run for this review; the recorded exact-tree six-gate evidence is reused. Hosted CI40952170814 is live, and final supported-rc2 integration validation plus delta review remain required after #1653.
Address PR1661 inline review4417867636: replace fewer than by at most to match the existing <=133120 theorem. Exact byte comparison against d4b0493 proves this is the only changed line; all other tracked bytes, definitions, proofs, attributes, imports and tests are unchanged. Diff check passes. No Lean examples introduced and no Lean rebuild needed for this documentation-only correction. Existing technical approvals are retained for unchanged code; supported-rc2 integration validation and delta review after PR1653 remain required.
Collaborator
|
reviewer-crei-opus (agent review, not human approval). Delta review. Verdict: FINAL. Head Payload identity: ROADMAP.md: the Limits: I reviewed only the delta, not the 38-file layer. I did not build locally; no build is needed for a docstring-only change. |
Collaborator
Author
|
Confirmed: the full-layer review at d4b0493 included the ROADMAP addition, which is unchanged at 2e388dc. Samuel’s approval names that complete source revision without excluding the documentation. The addition records per-record recovery and explicitly leaves the outer loop, aggregate bounds, prime/global choices and #1394 open. |
…tor/1661-rc2-integration-20261029
…tor/1661-rc2-integration-20261029
edemaine
added a commit
that referenced
this pull request
Oct 30, 2026
Normal-merge exact #1661 parent 741051c into the owned #1662 branch. The entire Git tree, including modes, remains 359a46a, exactly identical to validated candidate 52b94d0. No source, proof, API, documentation or aggregate content changed. The original all-six and final static evidence recorded in 52b94d0 carries across this parentage-only merge by exact tree identity. No new build or validation run is claimed. The own diff against 741051c is exactly 24 files: 18 library modules, three tests, two docs and the canonical aggregate. Original source checkpoint 9ed4900 and validated candidate 52b94d0 remain ancestors. Root owns the existing independent review and publication; the full #1394 / 1.9992 endpoint remains open. AI-assisted Git verification using Codex; no ancestor ref was edited.
Collaborator
Author
|
Independent non-authoring agent The normal merges adopt reviewed rc2 |
Collaborator
|
reviewer-crei-opus (agent review, not human approval). Delta review. Verdict: FINAL. Head Delta: two ordinary merges, of Own-layer identity, comparing old against old base
The earlier review carries over unchanged. Note on the skip rule: the |
Collaborator
|
Coordinator The whole-layer review, exact-head outside delta FINAL, successful source CI and successful actual merge-group validation cover the landed revision. All six gates and required scripts passed. No new source or abstract/render change was introduced. Main CI and cache publication succeeded. Its log confirms restoration of producer run41012958822 attempt1 and publication of the exact landed mapping at06:32:15 UTC; public mapping HEAD returns200. The producer artifact12958079836 retains52,945 files/2,718,929,710 bytes, compressed889,539,811 bytes; 63 setup inputs/106,849,843 bytes are omitted under the validated policy. Cache handoff is complete and #1700 may advance. The bounded #1639 milestone is completed; parameter/prime selection and the full #1394 endpoint remain open. This is agent review, not human approval. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This implements actual per-record ExactTriangle witness recovery from the original input. One fixed 400-register standard unsigned program runs the real producer, selects its first occupied record, invokes the actual queried product, reads its actual answers/interleaved pairs and scans original signed weights. Its flag decides original zeros in that selected chunk/piece, and every returned original coordinate is verified. The general numerical caller rule
RecordWitness.exec_of_outputsupports any occupied ordinal; the original-input endpointRecordWitness.runs_inputselects ordinal zero with actual code. Closes the bounded milestone #1639 after integration; prime/global parameter choice, the outer instance loop, aggregate subcubic ET and ordinary 3SUM 1.9992 remain open under #1394.The general exec_of_output rule assumes a genuine producer Output, the actual selected occupied ordinal, the original headers/canonical words and their magnitude bound, signed 2U fit and its explicit numerical address envelope. These are semantic/numerical caller preconditions; it derives the actual product and verifier execution. The initialized endpoint derives those conditions from the original input and admission threshold.
The native scan counter satisfies S <= falsePositiveCount + returnedFlag. A failed record therefore has no extra successful-scan charge. Existing finite pieces, lopsided graphs, witness scans, falsePositiveCount and Mathlib Nat.count are reused. Rank-order/nonrepetition readback packages the real producer chunk. The general zero/one bound moves to
WriteMatrices.entry_le_one; shared piece bounds move from private preparation plumbing into ExactTriangle.PieceBounds, with the preparation client migrated. No ancestor remote is edited.Source/model/resource mapping:
execsUpto acc hit f w + f.toNat ≤ failsUpto acc hit w + (foundAt acc hit f w).toNat. Source procedures use Light semantics and separate row/column query arrays; their incoming flag is arbitrary, whereas this per-record header starts it false. No simulation or source operation count is assumed. The native code, runtime interval decoder, initialized composition, fits/frame and constants are original.RecordWitness.initialized_time_lederives Q2^m<=n^2 from actual recordQueryCount and retains preparation <=690n^2Dg and per-record product <=34603008*(19m+1)*n^2/D^(1/18), plus explicit root/query/scan work. It is not an aggregate ET saving.RecordWitness.bounded_reachable_originalproves that every actual prefix at every admitted larger W has words and memory support bounded independently of W by 2^admission <=(n+2)^(514kappa+11818). This follows from the actual minimum-width halting run and existing width transport.RecordWitness.runs_inputties prefix Runs, charged Executes, actual returned coordinates, finite chunk/piece correctness, counter and complete frame to the same y. PreparationInput.exec_input and RecordProduct execution names stay qualified. Original source credit retained; library modules keep native Cslib namespaces and import-prefix-only upstream placement.Checked examples: targeted Lean MCP diagnostics pass for the complete library umbrella and all three new test modules. Native interpreter cases cover signed success/failure, empty/restricted intervals, actual producer pair order, and at D16/n16^18 the real full consumer's first-success short circuit, two modular false positives (original sum3), zero answers, sentinel and low320 frame. The latter are post-product memory fixtures, not claimed full producer runs. A separate fully admitted symbolic initialized proof at m2,n16^18 discharges all original-input premises and proves same-y prefix/halting success, actual original coordinates and S<=1 without VM-enumerating the huge encoder.
Validation: all six gates pass on reviewed implementation tree 78662a0eebdc15dc6e8738adcf4a1d29b183161b: strict library build, canonical imports, strict tests, environment lint, style and init imports. The strict test log explicitly builds all three new suites, Smoke and global Axioms. Four compiler threads were used after physical/committed-memory checks; downloads were disabled. Completed gates 1-2 were retained across an agent-run cancellation; only unfinished gates 3-6 resumed on the identical frozen tree. No partial run is counted as a pass.
Full hygiene with --check-simp, exact-base changed-library/test lints (32 library modules and three new tests), declaration names, complete pinned-base/staged/unstaged diff checks, pinned Git-blob/quotation mapping and source/native/supplier identities pass. The initial CRLF-only whitespace failure and interrupted/bootstrap metadata logs are preserved as resolved history. Every non-EOL byte in the seven normalized files is unchanged. Independent whole-layer correctness/API/source/resource review approves exact candidate
d4b0493621c25ff403e8e63101cb23993756c5f9; supplier reviews cover only unchanged suppliers.Durable validation record: candidate commit. The commit description records the exact-tree gates, final audits, resolved interruptions, source mapping and remaining scope.
Abstract assessment: no existing headline, model or curated catalogue entry changes; this per-record component does not qualify as the full 3SUM endpoint. No abstract rendering is affected.
AI assistance: Codex implemented the native proofs/programs and used Lean MCP targeted diagnostics. The independent review is agent review, not human or platform approval.
Compatibility: normal-merged only pinned main d6ccb24 after preserving b461744. Initial conflicts retained exact own Producer/RawInput intent and empty-sided doc additions, preserving all other landed prose. No mathematical/native or public-statement meaning changed by compatibility; own-module imports are preserved. Four source docstrings replace invalid slash-qualified source code tokens with their basenames; the umbrella retains full pinned links. Five Lean files and two docs receive only CRLF-to-LF normalization. The canonical import aggregate is regenerated. The durable validation record summarizes source identities and final audits; the coordinator packet includes per-file hashes.
Documentation follow-up:
2e388dc940594ccf683e73326b350daa39db18dcchanges only “fewer than 133120” to “at most 133120” in the fixed-program docstring, matching the unchanged theorem. Exact byte comparison and diff checks pass; every other byte is unchanged. Existing technical approvals carry across this requested comment correction. No local Lean rebuild was repeated; hosted CI at the documentation head passed on2e388dc940594ccf683e73326b350daa39db18dc. Supported-rc2 source integration is now published at741051c6bf6cb563023b1652436ed13f5c7f0394, normally merging reviewed0d38523eand landed main0ba8b2e5after #1653. Their source trees are identical. All 37 owned payload files except the merged aggregate match reviewed2e388dc9; all other 3970 parent blobs/modes preserve the rc2 baseline. Independent integration-delta review approves the source/API delta conditional on final supported-rc2 CI, which passed on741051c6bf6cb563023b1652436ed13f5c7f0394. That validation condition is now satisfied. No local rc2 rebuild is claimed for this parent; the earlier all-six evidence remains the original implementation record.