feat(ExactTriangle): derive uniform subcubic component budgets by edemaine · Pull Request #2148 · cslib-community/complexitylib

edemaine · 2026-11-01T09:33:25Z

Advances #1394 by removing the remaining logarithmic factor from #2147's actual native component allowance. This is a mathematical follow-up stacked on #2147; it adds no machine code and does not yet assemble the ET solver.

Cslib.Algorithms.WordRAM.ExactTriangle.DyadicCost.exists_components_subcubic_threshold proves: for each real κ≥1, one N≥2^1296 works for every n≥N, original matrices bounded by n^κ, selected prime and reference memory. The actual parameter-preparation allowance plus halt-inclusive selector and fixed-prime budgets is at most 4*n^(3−1/1296). Neither the threshold nor a running-time certificate is supplied to the algorithm. The numerical constant is shared; the threshold may depend on κ. Physical width does not occur in these component-budget functions.

The proof reuses Mathlib's isLittleO_log_rpow_atTop and Real.natLog_le_logb. It bounds the complete coefficient from #2147 by a κ-dependent constant times log(n), absorbs that into n^(1/1296), then combines it with n³/g≤4*n^(3−1/648). Quantifiers stay uniform: the threshold is chosen before matrices, prime, reference memory and positive-input proof. These are original conservative estimates, not Anthropic's tuned constants or a proof of its 1.9992 endpoint.

Kernel clients discharge all hypotheses for original constant matrices with weights0,1 and−1, obtaining actual selected primes and the same uniform reference-memory guarantee. They check an asymptotic cost result, not a giant interpreter run. One local library proof and one local test permit evaluation of the existing 1296-bit fast-threshold numeral; no heartbeat override is added.

Validation: the main theorem and all clients pass Lean MCP. Strict scoped compilation passes for the new module/test and inherited dyadic-cost test. Scoped environment lint, canonical imports, full hygiene/simp, compiled doc/new-test checker APIs on fresh scoped outputs, strict body names and complete-base whitespace checks pass. Independent nonauthoring agent /root/subcubic_budget_review APPROVE at 97fbc0f9145e840ab484e5bcc0d7a88066ed9239, with no blocking source/API findings. It checked the complete coefficient, reused logarithm estimates, rounding factor4, final exponent, threshold quantifiers and all three constant-weight clients against the actual parent budget. It ran no builds or source changes. This is agent review, not human or platform approval; exact-head full CI remains required. Hosted exact-head CI must supply all six gates and the standard whole-library artifact check before integration; no local full-six claim. No inherited Lean/abstract source is changed.

Actual solver assembly and small-case execution continue under #2146. Callable-adaptation/control costs, final ordinary-host/width composition, and the tuned #1394/1.9992 endpoint remain open. No curated abstract/catalogue/rendering impact. AI assistance: OpenAI Codex proofs and tests; independent agent source/API review; no human approval implied.

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.

…n scope

…ntation

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.

…source prose

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.

Source-complete #1701 checkpoint. Fixed128-bank standard program from raw(n,p) and3canonical signed matrices returns existing countZeroMod. Complete caller/State.init/same-y prefix/halt semantics and original arrays/outside dirty-workspace frame. Every setup/residue/index/table/padding/coefficient/Strassen-stack/copy/control/return/scan/halt instruction is charged: <=3704*(p+1)^2*(n+1)^(281/100). Runtime p factor remains explicit. Original p,A<=(n+2)^kappa imply sufficient physical width(kappa+24)*clog2(n+2), guaranteed input fit, and all wider prefixes have words/support below(n+2)^(kappa+25), independent of physicalW. No multiplication/layout/table/count/run/time oracle. Targeted Lean MCP clean for the complete umbrella, every new execution/width/prefix/time module, existing signed-array/Strassen/counter interpreter+kernel tests, and new fully admitted initialized clients: positive false-positive736steps, negative1454, signed asymmetric positive-depth4596, empty412, modulus-one354, and aliased-source dirty caller726prehalt with outside sentinel. Same-y Runs and charged halt are connected. Pin20e dependencies; bootstrap/initial failed target/MCP restart logs retained. Eight primary-source files verified byte-for-byte against pin16a5ce41304fcdaea4e0be7c132e1c361dc26da5; exact countOf_eq quote/locators checked. Source packet tmp/native-countprime-3dda8289/counter-{source-mapping.json,pr-body.md}. Canonical imports, final full static audits, hosted six gates and required fresh whole-layer nonauthoring review remain pending root coordination. No new-head all-six or review approval claim. No selected abstract/catalogue/rendering impact. Full1701 awaits validation/integration; prime selection2098, global ET/ordinary-host composition and1394/1.9992 remain open. AI assistance: OpenAI Codex. Original Anthropic credit retained; original4419 checkpoint preserved.

Local prerequisite integration into own #2098 branch only. Counter source and author credit are preserved; #1701 canonical/static finalization and independent review are pending. No counter approval or validation is inferred from this merge, and no ancestor remote is changed.

…ction LOCAL unvalidated source checkpoint for #2098. Prepares actual counter-call composition, uniform modulus budgets, a no-oracle caller selector endpoint and reuse of the actual9-instruction header plus6 copies. No new targeted Lean, imports/static audit, six-gate, independent-review or PR success is claimed; #1701 currently holds sole import/static slot. Previous checked component6b4068c3 is preserved. Resolve/check this source after explicit slot handback; full initialized admission/prefix/resource and #1394 remain open. AI assistance: OpenAI Codex.

Register 67 canonical imports for the source-complete #1701 counter at 61c82f6. No library/native/proof/test/doc source changed after that checkpoint. Final source tree including modes: 86adfee; pinned main20e3ba720ca7939a2ab65c1ada315d547551524e. Final validation: strict scoped --wfail/--iofail build of all69 changed library modules and4 tests PASS; the native counter umbrella environment lint covered all69 modules/1404 declarations and passed, and4 separately run test environment lints exited0. mk_all --check, full hygiene --check-simp, 6 strict PR-body names, complete base/staged/unstaged whitespace, and changed69-library/4-new-test documentation/restatement checks PASS. The standard changed-file driver encountered an unrelated missing global WordRAMUniformProbing.ilean; its unmodified checks passed with fresh own outputs and the available root inventory. No cold unrelated build was run. The redundant multi-root library lint remainder was stopped by exact owned PIDs after complete umbrella coverage passed, under resource pressure; its full-command successful exit is not claimed. Logs/dispositions preserved under tmp/native-countprime-3dda8289/final-*. No full-local-six claim: hosted exact-head CI must supply all six before integration. Source/supplier audit: 36 retained Strassen/array modules exactly match preserved4419; five native cyclic-kernel modules and its test exactly match landed20e; eight primary source files match pinned Anthropic Git blobs at 16a5ce41304fcdaea4e0be7c132e1c361dc26da5 and the countOf_eq quotation was checked. All76 changed paths are100644; policy/toolchain/dependency pins and abstract catalogue unchanged. No abstract/rendering impact. Fresh root-arranged whole-layer review is in progress; its bounds/width subreview approves61c82. Root reserves two nonblocking finite-source locator-only doc corrections after handoff. No review/integration approval or PR publication is claimed by this author. The actual fixed128-bank program computes existing countZeroMod, with original signed inputs/dirty caller frame, actual State.init and same-y prefix plus halt, charged <=3704*(p+1)^2*(n+1)^(281/100), original-input logarithmic width and physical-width-independent polynomial prefix support. The quadratic p dependence remains explicit. Selection2098 and global ET/ordinary-host/full1394/1.9992 composition remain open. AI assistance: OpenAI Codex; retained original Anthropic source credit.

Coordinator fixes the two optional source-reference nits from the independent whole-layer review of 61c82f6. Only two module-doc line ranges change: recurrence 81-96 and block identity/proof 105-126. No declaration, proof, native instruction, attribute, test, import or source-credit change. The parent 7bc9b1c adds only canonical imports to the reviewed source. Targeted/scoped compilation and audits remain recorded in that commit. Exact-head hosted six-gate CI remains required before integration; this documentation-only commit claims no new full local validation. Independent whole-layer review: #1701 (comment) AI assistance: OpenAI Codex.

Normal merge of pinned current main bc2e6c2 into approved source 02a7822. Git merged the aggregate and ROADMAP automatically; no manual conflict resolution. Identity audit: all 69 own library files and four tests are byte/mode-identical to the reviewed revision. Every other main source is retained exactly; only the canonical aggregate and preexisting counter ROADMAP/UPSTREAM additions differ from main. The 103-module local dependency closure of the counter and representative clients has no source delta. Aggregate imports exactly match the sorted 3586-module tracked inventory. Targeted MCP: counter umbrella, initialized execution tests and Strassen clients all clean (no errors/warnings/partial). Canonical mk_all --check, full hygiene --check-simp, body-name audit and staged diff --check pass. No full local validation rerun; hosted six-gate CI is required on this merged head. Original full six-gate coverage remains run41251234639 at 02a7822. Carry forward the independent whole-layer approval and locator/import delta approval only for the identical counter source. No new math/API/attribute or automation changes are introduced here. Full #1394 remains open. AI assistance: OpenAI Codex coordinator integration.

…selection Complete #2098 source on exact counter PR prerequisite4027bd980. The actual 160-register standard program enumerates the existing prime square window with native trial division, invokes the entire native cyclic-Strassen counter on original canonical signed matrices, and returns an attained minimum. Original arguments, dirty workspace and outside-source frames are derived; there is no supplied counter/run/time/prime-list/layout oracle. Generic caller plus actual15-instruction header yield original State.init prefix and charged halt in the same final state. Flat code<=32824 slots, no width reads. D>=16 suffices even for empty matrices or D>n. For D<=n, kappa>=1 and original weights<=(n+2)^kappa, positive sufficient physical width (kappa+30)*clog2(n+2) admits every wider execution; all successful prefix words/support are below (n+2)^(2*kappa+60), independent of physical W. Complete charge including header/halt <=3704*(sqrt(D)+1)^3*(n+1)^2.81 +42*(D+1); D dependence remains explicit. Existing IsSelectedPrime directly supplies the finite false-positive bound. Native tests prove actual update, stable ties and empty behavior; admitted clients connect actual State.init to selected prime3, exact count0, frame and the real source-regime FP theorem. Reuse the counter private numerical-admission proof by exporting it as CountPrime.admission_fits in its existing Width topic module and migrate its one internal client. Old counter public statements/programs remain unchanged. New modulus-budget monotonicity lives beside the actual counter/Strassen budgets. Abstract/catalogue/rendering unchanged. Source adaptation checked against Anthropic pin16a5ce41304fcdaea4e0be7c132e1c361dc26da5 ChoosePrime bytes17572 SHA256e9e7e9b8f8947d36043d8b1b8445a29d2ce90a004b2b88d8714f8701c1ec7280. chKeep/chRound95-107 policy reused; trial enumeration replaces the source prime-list producer109-118 and all native costs are independently proved. Validation at source checkpoint: targeted MCP checks clean through complete caller/header/input/width/flat/source/time composition and full initialized native test module, including actual kernel/VM clients. Canonical imports generated and check passes; hygiene--check-simp and full diffs clean. Source proof errors during development were fixed before these final diagnostics. Fresh whole-layer nonauthoring review, final scoped/static audit and exact-head hosted six-gate CI remain required. No local full-six claim. Global parameter/small-geometry/outer ET/ordinary-host composition and full #1394 exponent1.9992 remain OPEN. AI assistance: OpenAI Codex.

Implement #2127 as a child of reviewed selector1c290ca70. New original coarse family t=floor(log2(n)/1296), m=36t, D=4^m, g=4^t, L=19m. Prove g^36=D, D^18<=n for positive n, n<(4g)^648 and exact fast threshold t>0 iff2^1296<=n, which supplies D>=16. Small/zero inputs are classified, not assumed to satisfy fast geometry. These are not Anthropic tuned parameters or the final exponent1.9992 theorem. Actual fixed16-bank standard code reuses native NatLog and two Power calls; all logarithm/division/multiplication/power/copy/branch/header/halt instructions are charged <=12*log2(n)+36. At most128 flat slots inclhalt, no width reads. Generic caller uses original raw n and one derived word envelope; all memory and n are preserved. Original State.init[n], prefix, halt and all parameter outputs use one final y. Positive sufficient width <=12*clog2(n+2), every wider prefix words/support <(n+2)^13 independentW. New Power/Rename topic exposes the existing concrete execution in an injective bank with full input/memory/outside-bank frame, reused twice. Source/API paths: pure ParameterChoice and native DyadicParameters are new. All existing library/test files, especially the original15-register native Parameters splitting API, remain byte/mode-identical to parent. Only new modules, canonical imports and scoped coordination docs are included. No abstract/catalogue/rendering impact. Validation at this source checkpoint: Lean MCP clean for all new math and complete native initialized/kernel/VM suite, plus original chunk client. Actual VM boundary below/at2^1296, zero and dirty caller sentinel; fully admitted same-y original-input/kernel geometry and wider-prefix clients. One test-only exponentiation threshold permits this concrete1296-bit numeral; no heartbeat/recursion/axiom/sorry override. Canonical imports check and full hygiene--check-simp/diffs pass. Scoped strict/static checks and fresh nonauthoring review are next; hosted exact-head six-gate CI required before integration, no full-local-six claim. Callable fixed-prime solver #2125 proceeds independently; selected-prime composition, aggregate asymptotics, small-case solver dispatch, outerhost and full #1394/1.9992 remain OPEN. AI assistance: OpenAI Codex.

Implements milestone #2145 on exact #2133 f92e5c6, ordinary work/three-sum-native-et-aggregate-cost-20261101. Original conservative arithmetic on actual proved parameter/selector/fixed-prime charged functions: exact roots/powers, rounded query capacity, one global selected-prime scan reserve, selector absorption and explicit cubic-over-groups saving. Fast regime is n>=2^1296; original weights bounded by n^kappa, kappa>=1, actual existing selected-prime predicate retained. No supplied execution/solver/layout/time contract. n^3/g<=4*n^(3-1/648); logarithmic factors still explicit. This is not a composed program or tuned1.9992 endpoint. Strict scoped build PASS for DyadicCost, new WordRAMExactTriangleDyadicCost and inherited native parameter test; all new source/clients targeted checked. Scoped environment lint PASS; canonical mk_all check PASS; full hygiene --check-simp PASS; unchanged compiled doc/test checker APIs PASS on fresh two-library/one-test outputs; strict body names and full-base whitespace PASS. Parent library/test/abstract blobs unchanged; new source LF and modes0644. No local full-six claim; hosted exact-head CI must supply six gates plus the full standard artifact check. Scoped checker records4433 missing unrelated ileans explicitly, not a whole-library pass. Initial own RecordProduct.Flat cached read-only artifacts fixed only after nlink1/own-path verification; setup retry succeeds. Logs retained under tmp/et-aggregate-cost-20261101. Infinite dyadic-family client discharges actual fast geometry and original zero-matrix weight premises, obtains a selected prime, applies all component budgets and checks real-power saving. It is a kernel cost client, not an enormous interpreter experiment. Fresh independent whole-layer API/correctness review required before publication. No abstract/catalogue/rendering impact or claimed Anthropic tuned constants; existing hashing/scanning/native suppliers reused. Root1394 full ordinary-input/native-host/width/asymptotic composition remains open, with actual solver assembly separately owned under2146. AI assistance: OpenAI Codex.

Follow-up under #1394 on reviewed #2147 exact4e48de9e2 (all six hosted gates passed). One new original arithmetic module and one test; inherited native/math/API source unchanged. Reuses Mathlib isLittleO_log_rpow_atTop and Real.natLog_le_logb. For each real kappa>=1 one thresholdN>=2^1296 bounds every actual native parameter/selector/selected-fixedprime component allowance by4*n^(3-1/1296), uniformly over original three matrices bounded byn^kappa, selected prime, reference memory and physical width. Threshold is chosen before those data. Native component functions have no width argument. No time/run/layout/solver contract, no new executable code or effective threshold passed as algorithm input. Public theorem retains existing native budget's positivity proof explicitly, which also follows fromN. Original constants/tuned1.9992 not attributed or claimed. Main/new closed zero/+1/-1 constant-input clients pass targeted Lean MCP. Strict scoped build new Asymptotics module/new SubcubicBudget test/inherited DyadicCost test PASS19.99s; scoped environment lint PASS27.24s; canonical mk_all check/full hygiene --check-simp/scoped compiled doc+newtest APIs/strict body names/base whitespace PASS. Old source/abstracts unchanged, own LF/mode0644. Scoped checker records4433 unrelated missing ileans; hosted exact-head CI must supply full six gates and the standard full artifact check. No local all-six claim. Evidence under tmp/et-subcubic-budget-20261101. Fresh independent source/API review required before publication. One local library proof and one test permit1296-bit fast-threshold numeral normalization; no heartbeat/recursion override. Asymptotics proof absorbs all logarithms into half the previously proved1/648 saving. It proves component cost arithmetic only: #2146 actual solver/small-case assembly, callable adaptations/control, final ordinary-host/width/asymptotic composition and #1394 exact1.9992 remain OPEN. No curated abstract/catalogue/rendering impact. AI assistance: OpenAI Codex proofs/tests; existing supplier/source credit retained.

… time Complete #1394 milestone: natural dyadicTime depends only on original n and F; pointwise actual parameter/selector/callable ledger +42 is bounded for every selected prime and arbitrary reference memory. Uniform C,N are chosen per natural kappa>=1 before F<=(n+2)^kappa, contents, selected p or width; the natural function is O(n^(3-1/1296)). Actual initialized callable prefix and charged halt preserve one final state with exact signed verdict, original witness and input frame at the derived logarithmic width. Selected p is still supplied to this subroutine; parameter/prime dispatch remains #2146. No clock, layout, run or time law is an input oracle. Full #1394/1.9992 remains open. All final source MCP diagnostics clean. Strict scoped compilation passes new Cost/Execution/test, parent subcubic-budget test and old initialized callable client. Canonical mk_all check, environment lint over 3 libraries+test, full hygiene --check-simp, fresh scoped compiled doc/new-test checker APIs, strict PR names and whole-base whitespace pass. Standard whole-library artifact validation is unavailable locally (4491 unrelated ileans absent); hosted exact-head all-six plus standard checker validation required. No local full six claim. No machine program or curated abstract changed. Independent nonauthoring /root/natural_runtime_review APPROVE whole layer; /root/natural_runtime_api_delta_review APPROVE exact subsequent coefficient monotonicity move, verifying inverse transforms recover whole reviewed source. Review source hashes match final files. Agent review, not human approval. Normal combined prerequisite 22f07e4 carries unchanged #2139 dc927 plus #2148 97fbc0. Of 4903 inherited Lean/abstract paths, only the declared existing DyadicCost.Asymptotics coefficient API extraction is changed. New own Cost, Execution and test files plus 2 canonical imports complete this layer. Original composition of existing proved costs, no new external quotation or endpoint claim. AI-assisted by OpenAI Codex. Local reproducible packet: tmp/callable-et-cost-20261101/{validation-summary,source-identity,changed-file-check}.json and final-{strict-scoped,environment-lint,hygiene,pr-names}.log; public PR owns final validation and review. Detailed source mappings in module/PR text.

SamuelSchlesinger

Non-author coordinator codex-circuits-review2148-20261101, separate from the source-authoring context: APPROVE at 97fbc0f9145e840ab484e5bcc0d7a88066ed9239. No blocking correctness/API findings. I read the four-file layer and checked the exact parent budget; all 4,837 inherited Lean entries and pins remain exact #2147/4e48de9e. This approval reuses the unchanged component mathematics rather than commissioning another full review.

The theorem bounds precisely the parameter allowance plus halt-inclusive selector and fixed-prime budgets. The complete parent coefficient is bounded by a κ-dependent constant times log n; Mathlib's existing little-o theorem absorbs it into n^(1/1296). Combining that with the rounded n³/g≤4*n^(3−1/648) gives the stated numerical factor 4 and exponent 3−1/1296, without suppressing another polynomial in input length.

Quantifiers are correct: for each real κ≥1, one N≥2^1296 is selected before n, the original matrix-view data, selected prime, reference memory and positivity proof. The threshold may depend on κ; the multiplicative 4 is shared. Weight and selected-prime assumptions remain explicit, and physical width is absent from these budget functions. The result supplies neither a threshold to the machine nor an execution/ABI/width/input certificate. Callable/control adaptation, small-case execution, final host composition and #1394's tuned endpoint remain open.

Nonvacuous clients obtain selected primes and discharge all premises for original constant 0, 1 and −1 matrices, uniformly over reference memory; these are kernel budget clients. The local exponentiation allowances are explained, with no new heartbeat override. Documentation and title accurately describe component bounds, and there is no selected-abstract/catalogue/rendering change.

Hosted all-six CI 41289364386 / 124797198107 passed. Its verified finalized-log checkout 1522e09c has parents 4e48de9e and this head and exactly this head's tree. No local build/source change. This is approval of the stacked source; #2147 must land first and the resulting integration context still needs its checks. Agent review, not human approval.

SamuelSchlesinger · 2026-11-02T03:29:46Z

Prepared — bounded worker codex-prep2148-1730-20261102 froze unpublished ordinary merge fceb368e (tree fecf8e4b), with parents approved 97fbc0f9 and fixed actual main 66a6a0ca after #2147. Root's independent preservation audit is pending before publication; LogsQ retains fresh CI, retargeting, admission and cache ownership.

Both reviewed code/test blobs and modes, all 11 parent payloads and all 5,301 unrelated main entries are preserved. Only the generated aggregate and original UPSTREAM add/remove span needed resolution, with exact old-context guards. The complete original feature applies and reverses to exact main; 3,880 imports are canonical. The own delta is whitespace-clean; an inherited main-only EOF warning is recorded without unrelated edits. No proof/API change, Lean build, log retrieval, original-branch push, retarget, queue action or new approval. Original source ownership/credit and review 5729892929 are retained; component-budget scope and the full #1394 gap remain unchanged.

Merge fixed actual main66a6a0ca after actual #2147/b1d into the reviewed #2148 source97fbc0f. Resolve only the generated aggregate and the exact original UPSTREAM add/remove hunk, whose old context is byte-identical in current main. Preserve both reviewed code/test blobs and modes, all11 accepted parent payloads, and all5301 unrelated main entries/pins. The original complete feature applies and reverses exactly; the code-only feature patch is byte-identical. Validation is source-only preservation, canonical3880imports and own-delta whitespace checks. No local Lean/build or fresh full-six claim. The old-source-relative cached check reports an inherited main blank EOF at scripts/test_guide_selection.py:149; that file remains exact main, and the complete feature delta versus main is clean. Root independently audits this unpublished checkpoint before publication; fresh canonical full-six remains required afterward. Existing source ownership/credit and outside review5729892929 are preserved. No new proof, API, component-cost/asymptotic meaning or abstract scope. Full #1394 and actual solver/host assembly gaps remain. AI-assisted integration preparation: OpenAI Codex (codex-prep2148-1730-20261102), delegated by LogsQ. No new approval, original-branch publication, retarget or queue action.

SamuelSchlesinger · 2026-11-02T03:48:11Z

Coordinator logsQ-queue-20261101: #2148 is complete through actual landing and usable cache. Exact source fceb368e preserves outside source/API approval5729892929 and root’s independently audited carry5731912879, all original code, parent payloads and credit. Only canonical imports/original UPSTREAM replacement were reconciled; no new proof/API/meaning, abstract change or mathematical approval count.

Actual 851fa3f5 landed at04:14:34 UTC, sole parent 13e6a319, exact tree 78d85306. Both strict neutral orientations, both reviewed code/test modes/blobs, unrelated prefix entries/pins, 3,897 canonical imports and complete original feature inverse pass. Fresh source CI41384896288/job125083444517 passed all six at executed a9199618, parents [actual9f45d47b,fceb368e], exact neutral tree 435b08f9; own MQ41386230382/job125087567802 is terminal SUCCESS.

The immutable first-started covering main consumer41388282467/job125095495496, exact 60af788b, retains both #2148 payloads and all three #2276 tool/test/doc payloads. It passed all six and published at04:49:08.9801261 UTC. Mapping: 5,208 unique pairs, 234,373 bytes, SHA256 26810eb2b0923d4e48b887431986d5e69a212b3d817fd1c0a5b12224504a54d8; all18 new artifact references versus the saved verified 72a42fc3 baseline return positive-length HEAD200. One finalized main-log GET/one mapping GET, no duplicate baseline or artifact-body downloads. Optional handoff was unavailable; 28 library,24 test and6 abstract builds are recorded without restore-success/zero-rebuild claims.

This remains the reviewed arithmetic component-budget threshold chosen per κ before all inputs, independent of physical width. #2146’s assembled execution/control/host-width work and the tuned1.9992/full #1394 endpoint remain open. All own source/admission/cache holds for this completed PR are released. Agent coordination, not human approval.

SamuelSchlesinger

APPROVE the source-preserving main refresh — coordinator codex-root-2205-20261101, at fceb368e865c8a9dd30b80a64c44d08467516513, reusing the outside source/API review.

Both reviewed code/test entries and their complete code patch are unchanged. I independently applied and reversed the entire original nonaggregate feature, including the original UPSTREAM replacement, recovering the exact candidate and landed main without fuzz. All 5,301 unrelated main entries, pins, catalogue scope and canonical imports are preserved. No new proof, public meaning or source-credit change.

Fresh required CI and current-prefix validation remain before integration. This is agent review of preservation; the broader #1394 objective remains open.

Merge fixed actual main851fa3f5, containing actual #2139/6daf and #2148/851, into approved sourcec7b9fcf. The true own layer starts after joint parent22f07e41=[2148/97fbc0f,2139/dc92727d], not at the PR display base; inherited sibling code is not new feature work. Preserve all four reviewed code/test payloads and their documentation. Replay the complete original five-path feature, including imports, forward and backward exactly. Resolve only generated imports, exact reviewed Asymptotics bytes under main==joint-parent guard, and the unchanged-child ROADMAP conflict by retaining exact actual main. All5328 unrelated main entries/pins remain exact; imports are canonical3899. All28 callable payloads and107 parameter-branch code entries have explicit parent guards; the sole shared Asymptotics change is the already reviewed own-layer API/proof move. Validation is source-only preservation and own-delta whitespace. No Lean/build/CI-log download or full-six claim. The old-source-relative whitespace note is inherited exact-main scripts/test_guide_selection.py:149; no unrelated cleanup is introduced. Root independently audits this unpublished checkpoint before publication; fresh canonical CI follows. Original Edemaine/t3 implementation credit and outside review5729897050 are preserved. Supplied-selected-prime/component/asymptotic scope and full #1394 gap are unchanged; selected abstracts have no impact. AI-assisted integration preparation: OpenAI Codex (codex-prep2154-1730-20261102), delegated by LogsQ. No new mathematics, approval, source-branch push, retarget or queue/cache action.

cslib-community#2243) * feat(DataStructure): a doubling stack that grows inside its operations `Stack.Doubling` implements the bounded stack by a doubling array over the memory oracle: a push into a full array allocates an array of twice the capacity, copies the items (`Memory.copy`) and switches to it. It is a framed refinement whose footprint moves into fresh cells and whose room `4 C - 2 capacity` pays for its growth, so it shares memory with other growing structures. Every operation costs at most thirteen memory units, amortized. The tests run one doubling stack, two of them pushed alternately in one memory, and the two-stack queue over two doubling stacks, all through the generic allocator theorems. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure): adapt the doubling stack to allocators that take over cells `Allocates.le_footprint` is now `of_mem_footprint`, which allows cells taken over; the doubling stack takes over none. Products of allocators also ask for disjoint cells taken over, which is `Finset.disjoint_empty_left` here. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): Fibonacci heap over a record of named cells, part 1 (insert) (#2228) * feat(DataStructure/Memory): word-addressed memory oracle and named field arrays Memory.spec w is the memory oracle of #2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * doc(bib): add Guéneau, Charguéraud and Pottier (ESOP 2018) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials Refinement D E is a Module whose representation is an invariant plus an abstraction function (#2205 D2). Refinement.Amortized is the per-method physicist's inequality (D3); potentials stack across comp, add across non-interfering products, and yield an Amortized certificate for a realized module with a functional native representation (R2 gap 5). CostIsBigO is the exported asymptotic form (D6). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure/StateTransition): weaken and rescale amortized refinements Amortized.mono and Amortized.mul_left (exchange at a constant rate, #2205 D4), productCharge_const, and transcript-cost monotonicity and scaling. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure/StateTransition): place productCharge beside product, outside Refinement Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): make Refinement.Amortized a structure A Prop-valued def whose body starts with an implicit binder is unfolded and auto-introduced during elaboration against an expected type, which broke term-mode uses such as Amortized.prod. A one-field structure, like the existing DataStructure.Amortized, avoids this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: array stack over memory and queue method lemmas Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(Foundations): affine cost bounds are O(size) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * wip: queue over memory Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * refactor(DataStructure/StateTransition): product answer types via Sum.elim With a match, the answer types of product D E mention D and E through the matcher's parameters, so the elaborator cannot identify clients of two products whose components differ only in admissibility (for example the pair of stacks and the pair of bounded stacks). Sum.elim D.Result E.Result depends only on the component answer types. Queue.Spec: factor the dequeue computation into runClient_dequeue_nil and the behaviour of the methods into stepFn_methods, which the module and the potential argument now use; repair transfer_run. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): queue over two array stacks over the memory oracle The M1 slice of #2205. Stack.Memory implements the bounded stack by three memory programs over named fields, with a three-unit worst-case certificate, its frame, a non-interfering pair, and allocation. Queue.Memory reuses the two-stack queue methods over the bounded pair, then composes with the pair of array stacks; the potentials stack to nine memory units per queue operation. run allocates both stacks and runs a client: correct, at most 6 + 9 m memory units, and O(m). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * feat(DataStructure): Fibonacci heap insert over a record of named cells Add Record.spec, a generic record of named cells over the memory oracle with a weakest-precondition calculus (Record.wp) and a one-unit-per-operation refinement into Memory.spec. Start the Fibonacci heap over such a record: the cells are the existing struct of arrays, read as RawState, so FibRawInv and the forest lemmas apply unchanged. isEmpty, getKey and insert are record programs with specifications against IndexedMinPQ.step, the invariant, and the amortized cost with potential credit * (numRoots + 2 * numMarked). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG * fix(DataStructure): credit Renfei Zhou in the record Fibonacci heap; test records and insert Retain the original authorship of the native WordRAM Fibonacci heap that Basic.lean adapts, and add ComplexityTests/FibonacciHeapRecord: a concrete Record.Layout with a program run through Record.wp and Record.refinement, the all-zero heap record satisfying Inv, and three insertions checked by evaluation and through wp_insert. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> * feat(ExactTriangle): derive uniform subcubic component budgets (#2148) * feat(exactTriangle): relate lopsided queries and matrix products Adapt the finite counting interface and signed digit expansion from anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5 for milestone #1438. This is a mathematical interface; native preprocessing, fast solvers and full composition remain under #1394. * feat(exactTriangle): prove modular counts and the selected-prime bound * doc(threeSum): cite the lopsided triangle paper and clarify adaptation scope * doc(bibliography): sort the new paper entry * fix(exactTriangle): repair the prime-window header and hashing documentation * feat(exactTriangle): split modular queries and recover witnesses 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. * doc(threeSum): record finite splitting and recovery milestone 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 e41e1dda62a10c8f89917e2ccab54fbbedad1ad4, whose six strict gates pass. Checked the diff, milestone reference, implementation paths, hygiene and changed-file lints. Abstracts and rendering are unaffected. * refactor(exactTriangle): reuse the natural residue bound and clarify source prose * feat(matrix): prove the tensor recursion and pruned evaluation core * doc(matrix): clarify the overlapping contributing leaf * doc(matrix): make tensor and pruning explanations standalone * feat(wordram): count Chan–He collisions with native histograms 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 8e182b091199b323c7e6271acebbfcee2e4cdd18 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. * fix(wordram): preserve collision-counting parameters explicitly * feat(matrix): prove finite thin-product correctness and sparse bounds 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 b021e2d9340b433a9fdb129882351e158e8c289f, reusing the prior mathematics review. These are internal agent reviews, not outside coordinator or human approval. Source: anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, 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. * feat(wordram): compute Chan–He parameters from native input 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. * doc(matrix): explain finite thin-product guarantees in the Lean API 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 ee288fb16 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 b021e2d9340b433a9fdb129882351e158e8c289f in ee288fb16. 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. * fix(wordram): repair parameter proof hygiene and ceiling-log docs * feat(wordram): implement shared tensor encodings Complete the shared left/right encoder milestone #1493 above parent b4936ce28 (#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 b598513f02cc064eaf50d3c680684c19289ffd71 against b4936ce28d8b498b364a7947d34f728c55f8b226: 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. * test(wordram): connect encoder witnesses to charged runs 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 ad3e09735a116f9868e87cf7ae6af59e5cb6a285 (tree b598513f02cc064eaf50d3c680684c19289ffd71). Validation of tree 8277017f2c63a5851b63a5d4b49775a9fb96d62d against actual parent b4936ce28d8b498b364a7947d34f728c55f8b226: 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 ad3e09735/tree b598513f, 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. * feat(wordram): checkpoint native pruned-query controller proofs 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. * refactor(schonhage): reuse binomial bounds and sharpen signed tests 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. * feat(WordRAM): prepare and encode every shared matrix band 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@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, 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 bdfc5a1a33f0d712b90f4fe4bc9d6c27e2d8318e. 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 3b9234da6bc3c0daad2cd167aeb4fd8f9fc592b6. 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. * feat(wordram): checkpoint native pruned accumulation and frame transitions 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. * feat(wordram): checkpoint actual pruned-query root-frame stores 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. * fix(nat): reuse existing tuple digit identity in band preparation Address the sole P2 finding from the independent #1523 review of cb261f6b: 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 4807cb971cf8030f70df67e5e8fa13947dcbd202: 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: https://github.com/cslib-community/complexitylib/issues/1523#issuecomment-6479696830 Original implementation/validation handoff: https://github.com/cslib-community/complexitylib/issues/1523#issuecomment-6478943178 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 cb261f6b. * feat(wordram): checkpoint complete native pruned-controller phases 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 7fa4da67ea861a2bba3a6c430cd7e40996d0e794. 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. * doc(matrix): replace copied source prose with API descriptions Resolve the documentation-only requested changes on #1464: https://github.com/cslib-community/complexitylib/pull/1464#issuecomment-6477111132 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 4f3226cd 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 8c3b87bb870d4c4e2202917357d19a7a139296e8. 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. * refactor(finset): use order-embedding names in OrderGlue 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: 0c21b608cc5ed234527c73a3853a26132f52da0d. 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. * feat(WordRAM): prove all-depth pruned controller execution 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 f276db1174333d3e6253b93878be8b95c1fcc713; 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. * style(WordRAM): normalize native proof file modes * feat(wordram): complete initialized sparse pruned-query execution Complete implementation candidate for #1526 above #1520 exact 3b9234da6bc3c0daad2cd167aeb4fd8f9fc592b6. Full ordinary native 3SUM and the published 1.9992 endpoint remain open under #1394. No PR yet; fresh exact-revision independent correctness/API/source review is pending before publication. One fixed standard native program: 96 registers, at most 4096 flat instructions including halt, no width reads. Complete State.init -> pre-halt Runs -> Executes uses the same answer memory. Every supplied query, including repeats and empty/zero-depth boundaries, equals existing Pruned.result; runs_bilinear specializes existing encoding contracts to bilinearProduct. exec_kernel computes its powers/layout and has a reusable pointer/epoch directory contract. All child lists, timestamp decisions, stack/control/index arithmetic, signed products/adds and reporting are actual charged code, proved by the all-depth exec_ready induction; its continuation is discharged by the actual root exit. Full charge including halt <= 8192*(L+Q+1+(L+1)*card(leaves(requested qs))). Ordinary source envelope M=A+B+10^L*A*B and address budget H=256*(L+1)*10^L+32*Q+512 derive input fit and execution at every physical W >= clog_2(M+H+1)+3. This is logarithmic in explicit component budgets; global 3SUM composition is not claimed. Inputs: raw L,Q then two canonical signed arrays of length10^L and unsigned query codes, after the actual standard length cell0. Returned output pointer is unsigned. All input/outside memory is preserved on initialized runs. Code/ExecWithin/State.init/Runs/Executes, signed kernels, Heap/Block APIs, existing mathematical pruning/encodings and Mathlib digit/log APIs are reused; GenericRAM/Signed/Fits is the unchanged blob from #1552 f276db1174333d3e6253b93878be8b95c1fcc713, with credit retained. Pinned source anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. Checked Git-blob quotation locators: ThreeSumApsp/Sec2/Lemma10.lean:148-150 (Pruned_eq_restrictTo_sum) and:565-566 (Lemma10.total_size). Source Pruned -> existing Pruned.result; source restriction -> Finset.piecewise; source Leaves -> leaves; all natural depths and arbitrary integer arrays retained. Native indexing directly uses existing leafIndex(privateLeaf), first coordinate least significant, inner digit9. Child prefix/stride/division are proved against the finite childSet/sliceAt semantics. Native code/proofs and cost are original, not supplied by source Light semantics or its sorted-segment implementation. Full checked quotes and model/quantifier/layout/cost/reuse mapping are in the prepared UTF-8 PR draft. Copyright retained in source/NOTICE. Validation on tree bd6e74cce28dbd16c90291b847dac1a311402510: all SIX strict gates pass together, LEAN_NUM_THREADS=1, downloads disabled: build --wfail --iofail; mk_all --check; test --wfail --iofail (including Smoke/global Axioms); lint; lint-style; checkInitImports. Full citation-aware hygiene --check-simp; actual-base47-library/3-test changed-file and local lints; strict PR declaration-name audit; staged/unstaged diff checks pass. Register alias docs fixed the first lint finding; all native definition bytes are unchanged by that fix. Tests discharge real State.init positive/negative/empty/depth-two mixed/shared/repeated queries, sufficient-width family and failing fit boundary; callable signed wildcard with nonzero epoch and preserved input/outside sentinel also checks. No sorry, custom axiom or native_decide introduced. Selected abstracts/catalogue/rendering: no impact, no new headline. ROADMAP/UPSTREAM preserve the open sparse-product/ET and global1.9992 gaps. AI-assisted implementation by codex-three-sum-continuation-t3-3dda8289 (OpenAI Codex); original finite source credit to Anthropic, PBC. * feat(wordram): checkpoint computed wanted-query routing Partial implementation of #1561 by codex-three-sum-continuation-t3-3dda8289. Implements actual fixed standard 96-register routing/grouping code with computed valid-mask tables, tile counts, prefix offsets and stable scatter. General checked proofs cover the digit kernel (15L+10), one-query routing (15L+25), exact outStrOfPos/queryIndex mapping, computed header/count/relocated-table initialization (16L+(12L+33)*2^L+83), input-memory frame and original-input-derived fits. Generic finite stable-counting positions are injective and bijective. Targeted Lean MCP diagnostics clean for all nine new library modules and the regression suite. Actual initialized interpreter regressions pass for empty input, zero depth, duplicates and an asymmetric K0=2 three-band case; no encoded leaf array is materialized in routing tests. The 96-register program computes every routing/count/prefix/scatter decision. INCOMPLETE: general native counting, prefix and scatter execution invariants, initialized flat complete-run/width/frame/bound clients, final static hygiene and ALL SIX gates remain pending. This checkpoint is not a PR or acceptance claim. Mutable global audit slot remains with parent; no aggregate performed here. Full #1394 native sparse/ET solver and ordinary 1.9992 endpoint remain open. The child branch merges unchanged #1554 at 12abeee84 onto frozen #1562 base 0c2e0ebea. The local merge 60bec64398 only reconciled shared credit/roadmap/upstream prose; no ancestor branch was edited. Original implementation mathematics/code by Erik Demaine with AI assistance. Existing finite Schonhage and band/encoder/pruned interfaces are reused with their original credit retained. * feat(wordram): checkpoint wanted count-pass proofs Continuation of #1561 from 06b3563e7. CountStep has clean targeted Lean MCP diagnostics, including exact 14-instruction native count update and memory frame. Dense zeroing and count-loop composition are implemented; Count.lean has one pending elementary nonnegativity/address-bound proof at line 152. This is an explicitly incomplete source checkpoint, not all-six validated or a PR. Work is paused solely to prioritize the bounded outside-requested #1562 repair. No program/public statement in #1562 changed. * doc(finset): restore ordered-gluing source credit Restore the original AlmanWilliams2026 Section 2 citation and finite-scope sentence removed by the naming refactor. No Lean declarations or proof tokens change. AI-assisted coordinator fix by coordinator-codex-queue-20261028-ready-c. Original implementation and source authorship retained; independent delta review and new hosted CI requested on PR #1554. * fix(wordram): address pruned-query review findings Bounded documentation/test repair for #1562 / #1526 by codex-three-sum-continuation-t3-3dda8289, above exact 0c2e0ebea6199ac1fbe9b2e048ce24b9410f8d1a. Fix both ROADMAP reference definitions, distinguish client contracts from exported internal stage APIs, and document why the narrow ArrayAppend/InputArray topics avoid Allocation interface/dependency fanout. Extend existing post-integration issue #1553 with the exact pruned power register map, 4L+10 accounting, affected consumers, fused-encoder accounting and sibling integration order; no power program or ancestor is changed. Add one fully admitted signed runs_bilinear client: depth0, original arrays -3 and 2, actual encodingL/R premises discharged, original-input magnitude/address fits discharged, physical width10, same actual State.init prefix Runs and charged halt, and output memory at address6 equals Signed.encode(-6). Targeted Lean MCP diagnostics pass. Validation: all six strict gates passed together on final staged tree f4cfd4ae0d838c4b4bf4c43c924f400744450957, including Smoke/global Axioms; one thread/downloads disabled. Full citation-aware hygiene --check-simp, fresh actual-base 47-library/3-test module lint, changed-file audits, strict declaration-name check and staged/unstaged diff checks pass. Local machine-readable evidence: .lake/codex-three-sum-continuation/pruned-review-repair/{summary.json,static-summary.json,identity.json,*.log}. Source identity audit against 0c: all seven changed library files have identical comment-free tokens. Every public library statement, definition, native program and proof is unchanged. Every existing test byte is unchanged except the single inserted concrete client. Abstract/catalogue/rendering assessment: no impact. The prior inside-fleet technical review at issue1526#6484055995 and outside FINAL at PR1562#6484177608 cover unchanged native semantics/source mapping. Fresh focused outside review of this repair is requested; no new review agent was commissioned, and no outside/human/platform approval is claimed. All original Anthropic, PBC credit retained. AI-assisted implementation by OpenAI Codex. #1561 source is preserved separately at 7772a3497017078b37d1e04004225fae28baddad with its pending native grouping proof work explicit. Concrete sparse-product/Exact Triangle programs, full input/time/width composition and the original native 1.9992 endpoint remain open under #1394. * fix(imports): deduplicate aggregate after counting integration * fix(imports): deduplicate aggregate after query-splitting integration * fix(imports): regenerate aggregate after Chan-He parameter integration * feat(wordram): route and group wanted thin-product queries Implement #1561's complete native routing/grouping component. State.init prepends the native length cell to [L,m,N,Q] followed by raw coordinate pairs. Actual finite unsigned standard Code computes tables, tile keys, codes, counts, prefix offsets and stable scatter. No layout/run/time/permutation certificate is supplied. Fixed 96 registers, <=4096 flat slots including halt, no width reads. Wanted.runs_grouped proves actual State.init prefix Runs and charged halt at the same final memory, exact per-occurrence code/original-position equations, exact wantedStrings tile spans, in-array span/code bounds, permutation, terminal Q, input/outside frame and final boundedness. All admitted physical widths are covered by the positive clog2(wordBudget+1)+1 threshold, with original input fit derived. All initialized reachable prefixes are bounded. Complete native charge including halt <=128*(L+1)*(Q+numBands^2+2^L+1). No 10^L scan per query/tile. Validation: final tree 6c8164db02df348a46ffe0cf5972415977c62939. All SIX strict gates passed together: build --wfail --iofail; mk_all --check; test --wfail --iofail (including Smoke/global Axioms); lint; lint-style; checkInitImports. One Lean thread, cache downloads disabled. Full citation-aware hygiene --check-simp, fresh actual-base 57-library/3-test lints, changed-file/name/staged+unstaged diff checks all pass. The initial test-only module-boundary VM evaluation failure was fixed by using the existing non-module native-test convention; every interpreter check remains. The corrected frozen tree passed the complete six-gate sequence again. Base: #1562 ce77926c393ce34e7962759bb412172c4584a67c. Preserve normal merges. Unchanged sibling prerequisite #1554/#1536 is retained at exact 702c14bcf9896655b17c9b2dd5e02e6f270c9966: all 33 library and two test blobs are byte-identical. Wanted contributes 24 library modules and one test. Existing unchanged sibling reviews are reusable; no ancestor branch or remote was edited. Pinned source: anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, 3sum-apsp/ThreeSumApsp/Sec2/Theorem5.lean:44-46, checked against its Git blob: "outStrOfPos lay I J ∈ wantedStrings lay W (bandOf L m I) (bandOf L m J)". Tiling/Definitions.lean:128-131 defines that filter/image set; reuse it unchanged with W=qs.toFinset and separately preserve original list occurrences. Source Programs/Sec2/Theorem5/Wanted/Codes.lean:13-19 motivates routing. Actual native code uses the existing least-significant-first queryIndex/leafIndex dictionary, digit9 for the inner wildcard and 3*row+col otherwise. It proves agreement rather than identifying the Light program's separate numbering, semantics or costs. Native code/proofs/stable-scatter theory are original; primitive counts reuse Mathlib Nat.count directly, with zero/successor/bound/monotonicity APIs and the existing count_eq_card_filter_range identity. Redundant count/offset wrappers and their repeated elementary lemmas are removed. Every client is migrated; Program.lean and PackProgram.lean are byte-identical to checked checkpoint 2e2cc39675a30b024c3932bd23f06163a33c8925. Imported finite source credit is retained. All three source slices equal the pinned Git blobs. Fully admitted kernel clients cover empty/zero depth, repeated pairs, and the L4/m1/N110/K0=2 asymmetric family, tying answers to actual Runs/halt. Actual VM regressions cover all expected grouped words, original indices, offsets and input/outside frame. Fitting and failing physical-width premises are checked. No sorry, custom axiom or native_decide. No curated abstract/catalogue/PDF impact. Shared-band calls, actual buffer/header adaptation, pruned-kernel invocation, answer reconstruction, sparse-product/Exact Triangle and full native ordinary 3SUM composition/1.9992 remain open under #1394. This is a component milestone. Fresh nonauthoring correctness/API/source review is pending (root arranges); outside review remains required. No PR, integration or approval claim. AI-assisted implementation: OpenAI Codex, session codex-three-sum-continuation-t3-3dda8289. Author/source credit is preserved. * fix(imports): regenerate aggregate after shared-encoder integration * perf(wordram): reduce native parameter proof heartbeat budget * chore(wordram): scope measured parameter proof budget to reduction task * perf(schonhage): focus cell arithmetic and use the default heartbeat budget * fix(doc): restore unrelated upstream coordination records Restore the exact 231-line tail common to both integration parents after review caught an overbroad conflict-marker match. The intended 3SUM integration prose is retained; no Lean change. AI-assisted correction by OpenAI Codex. * fix(imports): regenerate band-preparation aggregate from merged inventory * doc(order-glue): preserve reviewed source credit through supplier merge * doc(order-glue): restore paper citation and finite scope * feat(wordram): checkpoint native queried-product construction (#1581) Unfinished implementation above exact a6e4005b2 on the existing isolated child branch. The fixed native program computes both producers, protected layouts/copies, tile ABI, one shared timestamp directory, actual pruned calls and original-order reconstruction. Targeted Lean MCP checks pass for the new native program and supporting original-input, parameter/layout, copy/frame, grouping-span, raw-conversion, producer and directory proofs. Five actual initialized interpreter regressions pass: empty, signed/duplicate, raw01, multiple tiles/padding/epochs, and nonempty inner tensor coordinates. This is a recovery checkpoint, not a complete native product result or PR candidate. Full tile/epoch loop and reconstruction correctness, initialized composition, complete charged cost and logarithmic-width/saving results remain open under #1581/#1394. All six/global/static validation remains held for root; no aggregate or static audit ran. Existing curated abstract statements and scope are unaffected; no headline promotion. Implemented personally by codex-three-sum-continuation-t3-3dda8289 with AI assistance. * fix(imports): regenerate thin-product aggregate after main integration * doc(wordram): separate shared-encoder integration records Keep the reviewed finite-matrix supplier records intact and record native-encoder scope and source credit separately, so squash-queue integration does not overlap the ancestor documentation hunks. Preserve code, tests, concrete bounds and the complete unrelated upstream-record suffix. Queue revisions are used only for read-only projection, never as parents. * doc(matrix): keep progress links out of shared reference append block * feat(wordram): checkpoint complete queried-product source before supplier merge (#1581) Local recovery checkpoint only. Complete native queried-product execution, initialized clients, quantitative thin saving and logarithmic width have clean targeted Lean MCP diagnostics. Import generation adds the 29 new modules. No all-six/static validation or independent candidate review is claimed by this checkpoint; it is not a PR candidate. The actual #1576 supplier advanced from a6e4005b to integration91f485ec. Preserve this source before a normal child merge, reconcile only shared docs/imports, regenerate the aggregate, then validate the final source together against the actual supplier. Original native implementation by Erik Demaine with Codex assistance, reusing credited finite Anthropic Section 2 mathematics and actual native producer/router/pruned kernels. Ordinary-3SUM/Exact Triangle and the full #1394 1.9992 endpoint remain open. * feat(wordram): execute queried thin-matrix products (#1581) Complete #1581 implementation candidate under #1394, awaiting required fresh exact-head non-authoring correctness/API/source/resource review. No PR is opened or integration approval claimed. Normal child history preserves source checkpoint af208636b and actual reviewed #1576 supplier91f485ec; no ancestor branch or remote was edited. One actual fixed standard unsigned WordRAM program per signed/raw input mode consumes original headers [L,m,N,Q], both row-major integer matrices X:N x 4^m and Y:4^m x N, and raw interleaved requested coordinates. It computes tables/layout, shared encodings, Wanted counts/prefix/stable scatter, tile pointers, decoded queries, directory/epochs, pruned evaluation and original-order reconstruction. Raw nonnegative entries are doubled by actual charged load/multiply/store instructions (including raw0/1 -> signed0/2). There is no source Light machine, assumed layout, sorting, solver, run or time oracle. QueriedProduct.exec/runs/runs_wide prove actual native execution from original words / State.init, same-y prefix Runs and charged halt, every original occurrence's exact Signed.encode((X*Y)[qs[i]]) including duplicates, original-input restoration and the complete outside frame. Generic execution assumes m<=L, original absolute entry bound A, raw nonnegativity in raw mode, and the explicit original numerical magnitude/address admission; it has NO query-sparsity hypothesis. The real pointer/epoch kernel uses a directory initialized once, with scratch/frame separation and propagated fresh bounded epochs. Code has 160 registers, <=32768 flat instructions including halt, no width reads, and is independent of dimensions, magnitudes, query counts and physical widths. Thin hypotheses: L=19m, D=4^m, N>=D^18. With distinct-set sparsity |qs.toFinset|*2^m<=N^2, complete charge including halt is <= 65536*(19m+1)*(65*N^2/D^(1/18)+Q). With the stronger occurrence hypothesis Q*2^m<=N^2 it is <=4325376*(19m+1)*N^2/D^(1/18). Multiplicity/output work is never replaced by set cardinality. runs_thin holds at EVERY physical W>= 128*clog_2(N+Q+A+2), deriving InputFits and all intermediate admissions. Its explicit magnitude/address envelope is <=2^40*(N+Q+A+2)^10, allocation <=128*(N+Q+A+2)^4. Physical all-prefix boundedness is proved; a separate source-polynomial prefix bound at arbitrarily larger widths is not extracted here. ET record/input adaptation and all its copies/calls, Exact Triangle solving, ordinary3SUM composition and improved Section4 / 1.9992 remain open. This component proves neither full3SUM exponent. Source mapping checked against actual Git blobs at anthropics/formal-math 16a5ce41304fcdaea4e0be7c132e1c361dc26da5, under3sum-apsp/ThreeSumApsp: - Sec2/Theorem5.lean:61-67 concludes the pruned band value equals (X*Y) I J. Existing finite thin_product_spec/MaskTable.layout/bandArrayL/R/encodingL/R and wantedStrings are reused; W=qs.toFinset, with a separate occurrence permutation. - Sec2/Theorem5.lean:146-149, paraphrase of its conclusion: ((sum T in tiles (19*m) m N, |Leaves(wantedStrings lay W T.1 T.2)|):Real) <=33*(D m)^(-(1/18):Real)*N^2. Source hypotheses N>=D^18 and W.card*2^m<=N^2 are retained. Existing encoding, tile/leaf/passed-set estimates bound ACTUAL native execution, not an assumed cost. - Programs/Sec2/Theorem5/Pruned/AllTiles.lean:86-92 and Wanted/Report.lean:30-37 are the per-tile/report specification references; Solver.lean:150-161 is conditional on Light callees. Native code here is original, accepts stable unsorted duplicates, charges empty tile calls and proves all native callees directly. Instruction constants, widths, protected layout and frames are independently proved for the native model. The UTF-8 PR mapping draft contains two exact Lean quotation slices, both checked against Sec2/Theorem5 at that pin; all four cited source files equal their pinned Git blobs. Anthropic, PBC's existing mathematical source credit is preserved. New native programs and execution/resource proofs are original work by Erik Demaine with Codex assistance. FINAL VALIDATION (whole source tree, not only this commit's proof/doc delta): Tree 555b6b52141f6e13f9f4aa913d6e7f7e5f8db474; four compiler threads; cache downloads disabled. 1. lake --no-cache build --wfail --iofail : PASS (13.56s). 2. lake --no-cache exe mk_all --check : PASS (11.33s). 3. lake --no-cache test --wfail --iofail : PASS (27.14s). 4. lake --no-cache lint : PASS (43.22s). 5. lake --no-cache exe lint-style : PASS (17.09s). 6. lake --no-cache exe checkInitImports : PASS (16.8s). Strict tests cover new initialized/product clients, Smoke and global Axioms. Full citation-aware hygiene --check-simp, fresh actual-base30-library/one-test lints, changed-file checks, 25-name strict final-body audit and staged/unstaged diff checks PASS. Actual comparison base: 91f485ec38ca6b878f338e2cdbdedbf5d4f20257. 3533 inherited source/abstract files checked; only the existing tile-key lemma is exposed with the same statement/proof. All35 inherited sibling blobs equal actual parent91. All native code bodies/register definitions are byte-identical to af208636b; comment-erased Program tokens match. Current full Program source SHA256: 2b86fe04f6afa49a7eadc75292559dca62f4d65c5f7bdaf3b1f4386994aa8ebc Public Header.exec_layout statement is identical; proof split passes at DEFAULT heartbeats, without a new allowlist entry. Final register docs clear the initial lint failure (47 undocumented aliases); prior incomplete/failed checkpoint logs are retained. Checked PR/source mapping draft SHA256: be43f587d5c0ac6dd871093d5d19c283ef7dd9732b5c5d3cfa77b24e42899a24 Local reproducible records: .lake/codex-three-sum-continuation/queried-product/ summary.json, static-summary.json, source-native-identity.json, source-mapping.json, run-identity.py, final-body-names.log and per-gate logs. This commit description is the durable evidence until a PR exists; issue1581 links it. Examples discharge real width/magnitude premises and connect the same final y to prefix Runs, halt and memory: signed/raw, duplicate, padded/multiple-tile, positive/zero depth, empty inputs, nonzero original header, adjacent sentinel, strict budget boundary and nonempty symbolic admitted thin family at every inner depth. Abstract assessment: no selected statement/definition/scope/catalogue/rendering impact. ROADMAP/UPSTREAM preserve remaining1394 scope; no headline promotion. Fresh review of all NEW native semantics/cost/width/frame/init/API/source mapping remains pending root arrangement. Unchanged prerequisite outside coverage can be reused after the recorded identities (1576 outside FINAL6487515809). No child watch/approval/merge. * style(Schonhage): remove trailing space in queried products Independent nonauthoring /root/queried_product_review examined the complete native #1581 layer at ff31104be7acf96798c13b38cb079c58605a1ec3 against 91f485ec38ca6b878f338e2cdbdedbf5d4f20257, including all 29 new library modules, actual execution/frame/width/cost, multiplicities, source mapping and initialized clients. No correctness/API/source/resource blockers; this is agent review within the root fleet, not outside or human approval. The single P3 finding was a trailing space in Product/Groups.lean:111. This coordinator correction removes exactly that ASCII space. An exact byte check and git diff -w verify no other change. Full base-to-head diff --check now passes, covering committed changes as well. All six gates and static/source checks pass on reviewed tree555b6b52, as recorded in ff31104. The whitespace delta is validated separately; final hosted CI and outside coordinator review remain required. Curated abstracts unaffected. AI assistance: Codex. * doc(Schonhage): retain band catalogue encoding contract Restore the one supplier sentence in UPSTREAM.md about unchanged leaf ordering and canonical signed words, addressing optional nit1 in outside FINAL6493515098 on PR1615. All other paragraphs are preserved. Exact byte comparison against9a57e134 verifies this one sentence is the entire tracked delta; all Lean/native/math/API/abstract source and every other tracked byte are unchanged. Documentation-only validation: consistency with the existing catalogue interfaces, full base-to-head diff --check, citation/simp hygiene and strict25-name final PR-body audit pass. No Lean, import, aggregate or full rebuild was run for prose. Original all-six evidence remains for tree555b6b52141f6e13f9f4aa913d6e7f7e5f8db474; this does not claim a new-head all-six run. No changed abstract meaning or rendering. Full nonauthoring native/source review and outside FINAL coverage are reused across this bounded doc delta. A focused outside DOC delta check is requested, not another full review. Register naming remains a separately coordinated follow-up; existing nonzero interpreter coverage was accepted, so no test change is included. AI assistance: Codex implemented the requested one-sentence documentation repair. * fix(imports): regenerate wanted-routing aggregate from actual inventory * wip(wordram): checkpoint callable thin-product source Personal #1618 source checkpoint before integrating the refreshed #1615 parent. Complete generic native memory-window compiler, computed-modulus callable raw01 product, initialized Runs/halt, width/window/cost and dirty-memory/frame tests have targeted Lean MCP diagnostics clear. Canonical imports and final all-six/static validation remain pending; this is not a publication candidate. Reuses the exact landed NatClog module from a1d1fa882, with original credit. No full Exact Triangle or ordinary3SUM endpoint claim. * feat(WordRAM): run queried thin products in caller-owned memory Implements the bounded callable prerequisite #1618 under #1394. Owner/session: codex-three-sum-continuation-t3-3dda8289, personally on work/three-sum-native-callable-product-20261029. Ordinary parent merge904c62068 preserves the reviewed #1615 a8cb7c984cd77e7eb150522e1353a2da22c84839 source. Generic MemoryWindow.compile adds actual add/load/remainder and add/store instructions, retaining ordinary Code/Exec/ExecWithin/Runs semantics. Proved bounded native-source execution transfers within3x charged instructions/code size, with3 additional registers and a full outside-window frame. The clipped memory view is a value relation, not another run semantics or an algorithm oracle. Concrete raw01 CallableProduct derives the actual source execution from original matrices/request occurrences. Native NatClog/Power compute the source modulus; fixed register normalization, translated producer/query execution and two exact input/output span-normalization loops are all charged. Fixed163 registers, <=131072 flat slots including halt, no physical-width reads. Actual initialized prefix Runs and halt refer to the same final data and exact requested products. Local input is restored and caller memory outside[b,b+M) is preserved. Thin admission is explicitly D=4^m,L=19m,D^18<=N, with raw zero/one matrices. M=2^(128*clog2(N+Q+3)) <= (2*(N+Q+3))^128. No whole-window or catalogue clear/copy. Every W>=256*clog2(b+N+Q+P+5) suffices. For arbitrary dirty callers P bounds EVERY initial register/memory word, including physical loads before remainder. For the initialized client scratch is zero and P only bounds the protected caller prefix. All-prefix assertions are physical word fits, not an independent-of-W polynomial intermediate-word theorem. The explicit window reservation is polynomial. Including base loading/halt: charge <=3*(originalT+1)+2048*(N*D+Q+1). Distinct-set sparsity retains+Q; occurrence sparsity Q*2^m<=N^2 gives 17301504*(19m+1)*N^2/D^(1/18). Neither sparsity premise is needed for execution. The ET-record adapter, fast ET/backend/witness composition and full ordinary3SUM 1.9992 remain open. Root retains parameters/prime selection/outer ET host. FINAL VALIDATION: tree f8ff0209469bb668837b9602fb71ecf3aaf3bc99. All SIX together PASS, four compiler threads, cache downloads disabled: lake --no-cache build --wfail --iofail (22.27s) lake --no-cache exe mk_all --check (13.75s) lake --no-cache test --wfail --iofail (183.59s), including Smoke/global Axioms lake --no-cache lint (45.02s) lake --no-cache exe lint-style (22.14s) lake --no-cache exe checkInitImports (16.56s). Final full hygiene --check-simp, actual-base12-library/two-test lints, changed-file checks, strict14-name PR draft audit, COMPLETE a8-to-final diff --check, staged and unstaged diff checks all PASS. Canonical imports generated; all new tracked file modes100644. No sorry/custom axiom/native_decide or new heartbeat override. Only justified finite syntax-check recursion-depth options. Source audit: all3686 inherited source/abstract files and modes unchanged from actual reviewed parenta8. Original Product, Wanted/Pruned/Band/encoding, NatClog and Power suppliers remain unchanged. New MemoryWindow and Callable/Program files are byte-identical to source checkpoint7cb7ade0a. ArrayNormalize native bodies and theorem statements are identical; the only API metadat…

edemaine added 30 commits October 28, 2026 08:52

feat(exactTriangle): prove modular counts and the selected-prime bound

dec963a

doc(threeSum): cite the lopsided triangle paper and clarify adaptatio…

0d8da3e

…n scope

doc(bibliography): sort the new paper entry

8d80ecc

fix(exactTriangle): repair the prime-window header and hashing docume…

fd69be7

…ntation

refactor(exactTriangle): reuse the natural residue bound and clarify …

dc4206a

…source prose

feat(matrix): prove the tensor recursion and pruned evaluation core

2434f47

doc(matrix): clarify the overlapping contributing leaf

62dc601

doc(matrix): make tensor and pruning explanations standalone

4f3226c

fix(wordram): preserve collision-counting parameters explicitly

a712205

fix(wordram): repair parameter proof hygiene and ceiling-log docs

0505439

style(WordRAM): normalize native proof file modes

a93c021

edemaine added 11 commits October 31, 2026 18:30

Merge reviewed counter PR prerequisite for native prime selection

12e121e

edemaine requested a review from SamuelSchlesinger November 1, 2026 09:33

edemaine mentioned this pull request Nov 1, 2026

feat(3sum): adapt Anthropic’s algorithm directly to WordRAM #1394

Closed

edemaine mentioned this pull request Nov 1, 2026

feat(ExactTriangle): bound initialized native ET by natural subcubic time #2154

Merged

SamuelSchlesinger approved these changes Nov 1, 2026

View reviewed changes

This was referenced Nov 1, 2026

feat(ExactTriangle): assemble a parameter-selecting native solver #2155

Merged

feat(ExactTriangle): bound native dyadic component costs #2147

Merged

SamuelSchlesinger self-assigned this Nov 2, 2026

SamuelSchlesinger changed the base branch from work/three-sum-native-et-aggregate-cost-20261101 to main November 2, 2026 03:46

SamuelSchlesinger reviewed Nov 2, 2026

View reviewed changes

SamuelSchlesinger added this pull request to the merge queue Nov 2, 2026

Merged via the queue into main with commit 851fa3f Nov 2, 2026
3 checks passed

SamuelSchlesinger mentioned this pull request Nov 2, 2026

ci(integration): verify canonical aggregate-only conflicts #2276

Merged

Navigation Menu

Repository navigation

feat(ExactTriangle): derive uniform subcubic component budgets - #2148

feat(ExactTriangle): derive uniform subcubic component budgets#2148
SamuelSchlesinger merged 165 commits into
mainfrom
work/three-sum-native-et-subcubic-budget-20261101

edemaine commented Nov 1, 2026

Uh oh!

SamuelSchlesinger left a comment

Uh oh!

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading

Uh oh!

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading

Uh oh!

SamuelSchlesinger left a comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

edemaine commented Nov 1, 2026

Uh oh!

SamuelSchlesinger left a comment

Choose a reason for hiding this comment

Uh oh!

SamuelSchlesinger commented Nov 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SamuelSchlesinger commented Nov 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SamuelSchlesinger left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading

SamuelSchlesinger commented Nov 2, 2026 •

edited

Loading