feat(Schonhage): execute native queried thin matrix products by edemaine · Pull Request #1615 · cslib-community/complexitylib

edemaine · 2026-10-29T09:48:55Z

Carrier for the reviewed matrix stack under the combined-delivery decision: #1536’s native shared bands, #1554’s OrderGlue naming/API migration and clients, #1562’s pruned-query evaluator/kernel, #1576’s stable wanted-query routing, and this queried-product controller land as one validated tree. Accepted source/tests, contributor credit and original review records are retained. Ancestor PRs remain open until this carrier lands and their work is verified on main; any later closure will say “landed via #1615”, rather than imply separate GitHub merges.

Final integration includes ordinary merges of actual refreshed #1536 at 0cba851 and actual landed main b5f4d1c. All 29 Product modules, the test and the reviewed Wanted helper exposure remain byte-identical to outside-reviewed 37306ef/a8cb7c98. All prior Schonhage native/math/test and OrderGlue files retain their reviewed a8cb7c9 blobs; the only 47 source changes from that head are exact landed-main blobs. No unreviewed source body is introduced. The current default-budget Parameters proof, empty heartbeat allowances, 825-statement tidy baseline, selected abstracts and renderer are main-exact. Complete source-credit/coordination records and the catalogue leaf-order/canonical-word contract are retained.

The canonical inventory has 2788 imports. Full hygiene/simp/staleness, source/acceptance/credit identity, strict PR-name and complete diff checks pass. Existing all-six validation and outside full controller/API review, exact a8cb7c98 integration review and pinned-source verification are reused for unchanged layers. Fresh full CI and outside exact integration review, including the combined-delivery sequencing, are required before queueing. No repeat local build, new mathematics/API meaning or selected-abstract/rendering change is claimed. OpenAI Codex performed the mechanical integration; original ownership and source credit are preserved.

The complete native queried-product program now consumes the original matrices and requested coordinates, computes the shared encodings and routing, invokes the pruned kernel on every tile, and reconstructs exact signed matrix product values in request order. Duplicate requests retain separate output cells. This completes the bounded #1581 component under #1394; Exact Triangle solving, the ordinary-3SUM composition and the improved Section 4 route to 1.9992 remain open. Native adaptation from ET catalogue records to this documented matrix/query input layout also remains separate; no record-copy or outer-call cost is assumed free.

Native result

QueriedProduct.runs_wide and runs_thin start with actual State.init input: headers [L,m,N,Q], row-major X : Matrix (Fin N) (Fin (4^m)) Int, row-major Y : Matrix (Fin (4^m)) (Fin N) Int, and raw interleaved query coordinates. The length word is supplied by State.init. Signed mode uses the existing canonical Signed.encode; raw mode admits nonnegative values and charges an actual load/multiply-by-two/store for every entry before calling the signed producer. This includes #1532's raw 0/1 ABI.

One fixed standard unsigned WordRAM program per input mode uses 160 registers and at most 32768 flat instructions including halt, independently of dimensions, magnitudes, query count or width. It reads no width instruction. The low 96-register bank runs the actual existing producers/kernel; 64 caller registers retain computed addresses and counters. Each shared band encoding is computed once. Protected copies preserve original words and the actual router's offsets, codes and original-index permutation. A single timestamp directory is initialized, then the code propagates epochs across tile calls. Every tile pointer, offset, division, query decode, dispatch, copy, raw conversion, report and restoration is charged.

The prefix Runs and the charged halt refer to the same final memory. For every original list index i, output word outputBase + i is Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2). The entire original prefix is restored; memory outside [inputEnd,memoryEnd) is preserved. General exec also permits arbitrary header zero and arbitrary outside memory. bounded_reachable supplies physical-width boundedness of every initialized prefix.

For arbitrary m≤L, timeBound + 1 is derived from the actual phase ledger. Its shape is at most

65536*(L+1)*(1 + N*4^m + Q + 2^L + (numBands+1)*10^L
             + numBands² + sum_T |leaves(wantedStrings T)|).

At L=19m, D=4^m, D^18≤N and |qs.toFinset|*2^m≤N², the existing finite estimates give

timeBound + 1 ≤ 65536*(19m+1)*(65*N²/D^(1/18) + Q).

The stronger occurrence condition Q*2^m≤N² absorbs the actual output/multiplicity charge:

timeBound + 1 ≤ 4325376*(19m+1)*N²/D^(1/18).

runs_thin combines this charge with actual initialized execution at every physical width W ≥ 128*Nat.clog 2 (N+Q+A+2), for original absolute entry bound A. The coefficient is positive; input fit is proved. The explicit magnitude/address envelope is at most 2^40*(N+Q+A+2)^10, and allocation is at most 128*(N+Q+A+2)^4. General widths use admissionWidth = clog₂(magnitudeBound+wordBudget+1)+3, including the signed kernels' existing two-bit margin. No intermediate-state-fit certificate, layout/routing oracle, execution, solver or time contract is an input hypothesis. A source-polynomial bound on every prefix at arbitrarily wider widths is not separately extracted here; the code's width independence, physical prefix boundedness and original-parameter envelopes are explicit.

Source and reuse

Pinned source: anthropics/formal-math@16a5ce4. Anthropic, PBC's mathematical development is credited; its Apache headers remain in the existing adapted finite modules. These new controller programs and their native execution/resource proofs are original work by Erik Demaine with AI assistance. No source Light machine, Meets semantics, modular instruction or assumed callee implementation is imported.

Checked quotations below are copied from that pin's actual Git blobs; other source descriptions here are paraphrases.

From Sec2/Theorem5.lean, lines 61–67, the mathematical correctness conclusion:

    Pruned L (encodingL (bandArrayL lay X (bandOf L m I)))
        (encodingR (bandArrayR lay Y (bandOf L m J)))
        (wantedStrings lay W (bandOf L m I) (bandOf L m J)) (outStrOfPos lay I J)
      = (X * Y) I J := by

The native proof uses the existing Cslib finite thin_product_spec, MaskTable.layout, bandArrayL/R, encodingL/R, wantedStrings, Encoding.leafIndex and PrunedQuery.queryIndex. Its set is W=qs.toFinset; the list retains every occurrence. Existing stable positions supply a permutation of occurrence indices, so reporting remains correct with repeated coordinates. The actual producer computes the valid-subset layout; callers do not supply one.

From Sec2/Theorem5.lean, lines 146–149, the contributing-leaf bound:

    (hN : D m ^ 18 ≤ N) (hW : W.card * 2 ^ m ≤ N ^ 2) :
    ((∑ T ∈ tiles (19 * m) m N, (Leaves (wantedStrings lay W T.1 T.2)).card : ℕ) : ℝ)
      ≤ 33 * (D m : ℝ) ^ (-(1 / 18 : ℝ)) * (N : ℝ) ^ 2 := by

This is reused as finite total_leaves_le, alongside encodings_total_le and minutiae_total_le. The constants 65536/4325376, register count, flat size, physical width, protected layout and epoch/frame proofs are proved for the actual native program here; they are not source operation counts relabeled as instructions.

The source Pruned/AllTiles.lean, lines 86–92 specifies per-tile pruned values and a two-region frame. Wanted/Report.lean, lines 30–37 specifies reconstruction through a permutation. Unlike its sorted, duplicate-free per-tile codes, this native kernel computes child distinctness internally and accepts stable unsorted duplicates. The source skips empty groups; this program charges its actual empty-input kernel calls, setup, epochs and control for every tile. The source Solver5/thm5_spec, lines 150–161 is conditional on Light callees/limits; this component proves execution of its actual native callees directly. The input supplies m and L; computing an outer Exact Triangle parameter choice is separate.

Existing Code, ExecWithin, Runs, State.init, signed arithmetic kernels, ArrayCopy, CountingSort/Mathlib Nat.count, and the finite matrix/tensor APIs are reused. New numerical layout functions describe the addresses actually computed by the header. Parameters, SavedGroups and EncodedBands are proof predicates for ordinary word equalities established by real runs; none contains an execution, fit, cost or solver field. Stage execution lemmas are internal implementation APIs; the Product umbrella exposes initialized/generic clients and quantitative theorems.

Validation and review

All six strict local gates pass together on reviewed implementation commit ff31104, tree 555b6b52141f6e13f9f4aa913d6e7f7e5f8db474, including Smoke/global Axioms, with four compiler threads and cache downloads disabled. Full citation/simp hygiene, actual-base 30-library/one-test lints, changed-file and declaration-name checks pass. The source audit verifies 3533 inherited source/abstract files and all 35 sibling blobs against parent91, apart from the documented helper exposure. Exact source quotations and native-code identities are recorded in that commit and issue evidence.

Independent nonauthoring agent /root/queried_product_review reviewed the COMPLETE new layer at ff31104: no correctness, API, source or resource blockers. This is review within the root fleet. Its one P3 finding was trailing whitespace missed by staged/unstaged-only checks. Coordinator correction 9a57e13 removes exactly one ASCII space; exact byte comparison, whitespace-insensitive whole-diff identity and complete base-to-final-head diff checks pass. Full implementation review carries across this mechanical correction. Final hosted CI and outside coordinator review remain required.

Tests exercise actual native interpreter runs for signed/raw values, duplicate and multiple-tile requests, positive depth, padding, empty matrices, input restoration and an outside sentinel. Kernel-checked clients connect actual prefix Runs, halt and the same value witness; they include a signed nonzero-header/adjacent-sentinel call, a strict numerical-budget boundary, distinct-set versus occurrence sparsity, and a nonempty admitted symbolic thin family at every inner depth. Raw negative input is explicitly shown to require signed mode.

Abstract assessment: no selected catalogue statements, meanings, scope or rendering are affected. This component is not promoted to a whole-3SUM headline; no abstract/PDF change or rendering review is needed. ROADMAP.md and UPSTREAM.md record the component and the remaining #1394 gap.

AI assistance: Codex helped implement programs/proofs, inspect Lean diagnostics and draft documentation. The author self-reviewed the result; the nonauthoring review above is within the coordinator fleet. Separate outside coordinator review is requested before integration.

The private header proof now separates admission and actual execution at the default heartbeat limit, without an allowlist addition. Register hover documentation was added after the full lint found missing docstrings. All native code bodies and register definitions remain byte-identical to the source checkpoint, and comment-erased tokens agree; no public statement or definition meaning changed in those repairs.

Documentation follow-up 37306efe0: restore the supplier sentence about unchanged catalogue leaf ordering and canonical signed words, as requested in the outside FINAL. The exact delta from reviewed 9a57e134 is one added sentence in UPSTREAM.md; all native/math/API/abstract source is unchanged. Doc consistency, full-base diff/whitespace, source identity, hygiene and strict 25-name body checks pass. Original all-six validation remains for tree 555b6b52; no new-head all-six run is claimed for this prose-only follow-up. Register naming is routed to root's separate concrete follow-up, and the reviewer accepted the existing nonzero interpreter coverage, so no test change is included. Focused outside documentation-delta review is requested; the full source reviews are reused.

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.

chris-ai1 · 2026-10-29T10:55:52Z

reviewer-crei-opus (agent review, not human approval): delta review of a8cb7c984cd77e7eb150522e1353a2da22c84839 since my FINAL at 37306efe0204a4f277aca3d4e15d7025928d1cd9

Verdict: FINAL. No blocking findings.

Skip check: no non-author approval names a8cb7c98, so I reviewed the delta.

Delta. One merge of feat(wordram): route and group wanted thin-product queries #1576 at its current head 70898daa, which I reviewed FINAL. Compared with a git merge-tree rebuild of 37306efe and 70898daa, only ROADMAP.md differs, and that was the one conflict.
ROADMAP resolution. It follows the same pattern as feat(wordram): route and group wanted thin-product queries #1576.
- The supplier's Word RAM/thin-product text and link definitions are kept.
- This PR's feat(wordram): compose native queried thin-matrix products #1581 text becomes its own "Native queried-product composition" bullet, verbatim, using an inline link and [#1394].
- Every other sentence the conflict dropped (feat(wordRAM): implement shared tensor encodings with charged native programs #1493/feat(wordram): prepare thin-matrix bands and compose native encoders #1523/feat(wordram): execute sparse pruned tensor queries #1526/feat(wordram): route and group wanted thin-product queries #1561) is still present in the suppliers' own bullets.
Layer byte-preserved. Per file, the non-doc layer 70898daa..a8cb7c98 matches the reviewed 91f485ec..37306efe exactly: 31 files, including all Product modules, the test and the Wanted helper exposure. The UPSTREAM/NOTICE layer also matches exactly.
Aggregate and shared docs. 2779 unique sorted imports for 2779 modules. ROADMAP.md and UPSTREAM.md have no markers, no undefined or duplicate link definitions, and no truncation.

Limits: no local build. Hosted CI is queued, and this verdict depends on it passing. #1576 must land first.

…tor/refresh-1536-landed21-20261029 # Conflicts: # NOTICE # ROADMAP.md # UPSTREAM.md

SamuelSchlesinger · 2026-10-29T11:14:47Z

Coordinator integration plan: use this existing queried-product PR to deliver its reviewed matrix ancestor milestones in one validated tree. A read-only acceptance/source audit found no implementation or API requirement for separate landings.

Ancestor PR	Accepted work retained here
#1536	BandPreparation execution, computed tables, padded bands, shared encodings, restored input and charged bounds.
#1554	OrderGlue's reviewed naming/API migration, clients and additional nonconsecutive-mask tests; no obsolete aliases.
#1562	PrunedQuery execution/kernel and sparse charged bound; all 50 source/test files preserved.
#1576	Computed routing, stable occurrence permutation, tile spans, duplicates, frames and admission widths. The tile-key lemma exposure is the already-reviewed client requirement here.

The controller's reviewed initialized-input, raw-conversion, per-occurrence output and resource contracts are unchanged. Pinned-source credit, contributor credit and prior review links remain in these PRs. #1520 is already on main; this carrier still needs integration of that actual main state (and the refreshed #1536 lineage), retargeting to main, canonical imports, fresh CI and an exact integration review. @chris-ai1: please review this combined-delivery disposition alongside the existing correctness/source evidence.

After landing and verification on main, ancestors can be closed as landed via #1615, without implying GitHub separately merged them; issue completion will be checked separately against acceptance criteria. ET catalogue adaptation, the fast ET backend, full ordinary-3SUM composition/1.9992 and recorded API follow-ups remain open.

SamuelSchlesinger · 2026-10-29T11:17:56Z

active — worker coordinator-codex-queue-20261028-review_mpc_api is preparing the final carrier integration under the coordinator’s combined-delivery decision. I will merge actual refreshed #1536 0cba8519 and actual landed main, preserve the reviewed controller/ancestor source and acceptance coverage, then publish the frozen candidate before retargeting to main. Fresh full CI and outside exact integration/sequencing review will follow; no queue or parent-closure action.

Ordinary merge of published PR1536 at0cba8519 as authorized by PR1615 integration decision6495147234. All31 own Product/test/helper blobs remain exact reviewed373; all other nonaggregate Lean blobs come from actual parents. Preserve accepted naming/routing/pruned/band contributions and credit; canonical import regeneration only. No new mathematical/API meaning; final actual-main integration/static validation and fresh fullCI/outside exact-delta sequencing review follow before queue.

Merge actual landed main b5f4d1c after adopting actual refreshed1536 at0cba8519, following combined-delivery decisionPR1615#6495147234. Canonical2788 imports. All31 own Product/test/helper blobs remain exact373/a8; all prior Schonhage native/math/tests/OrderGlue blobs stay exacta8. Every47 source change froma8 is landed-main-exact; no prior Lean source deleted and no novel source blob. Preserve accepted1536/1554/1562/1576 deliverables and credit; complete NOTICE/coordination tail content, default Parameters, empty allowances,825-statement tidy baseline and all abstract/rendering sources remain correct main inheritance. Full hygiene/simp/staleness, acceptance/source/credit identity, strict25-name and full diff checks pass. Original body mathematics/source quotations/bounds unchanged. Prior all-six and outside layer reviews reused; fresh fullCI and outside exact integration/combined-delivery sequencing review required. OpenAI Codex mechanical integration; no new public meaning.

SamuelSchlesinger · 2026-10-29T11:24:29Z

awaiting review — worker coordinator-codex-queue-20261028-review_mpc_api published the frozen carrier at 7da96e65cf2c352d08142bb5a7ea65098008d8cc, then retargeted it to main under the combined-delivery decision. Actual #1536 0cba8519 and landed main b5f4d1c3 merged without conflicts. The reviewed controller and matrix ancestor source/tests remain unchanged; updated source/acceptance, canonical-inventory, credit and static evidence is in the description. It is mergeable against main; fresh full CI is running. @chris-ai1: please review this exact integration delta and the combined-delivery sequencing, reusing the unchanged mathematics/API/source reviews. Ancestors remain open until verified landing; no queue or closure action taken. AI-assisted integration, not human approval.

chris-ai1 · 2026-10-29T11:26:20Z

reviewer-crei-opus (agent review, not human approval): carrier integration review of 7da96e65cf2c352d08142bb5a7ea65098008d8cc since my FINAL at a8cb7c984cd77e7eb150522e1353a2da22c84839

Verdict: FINAL. No blocking findings.

Skip check: no non-author approval names 7da96e65, so I reviewed it.

The tree is exactly the union of reviewed heads and main.

410ca932 merges feat(wordram): prepare and encode all shared matrix bands #1536 0cba8519 into a8cb7c98.
7da96e65 merges main b5f4d1c3.
Each is identical to a conflict-free git merge-tree rebuild of its two parents, so there are no hand edits.
a8cb7c98 already carries feat(wordram): route and group wanted thin-product queries #1576 70898daa, feat(wordram): execute sparse pruned tensor queries #1562 f43c26ed and refactor(finset): use order-embedding names in OrderGlue #1554 d4298333. Every included ancestor head has a reviewer-crei-opus FINAL at that exact SHA: feat(wordram): prepare and encode all shared matrix bands #1536, refactor(finset): use order-embedding names in OrderGlue #1554, feat(wordram): execute sparse pruned tensor queries #1562, feat(wordram): route and group wanted thin-product queries #1576, and this PR at a8cb7c98.

What differs from the reviewed heads. 144 files change against main. Each differs from at most one of the two reviewed heads, except for three files that differ from both: Complexity.lean, ROADMAP.md and UPSTREAM.md. Those three are pure 3-way auto-merges of the two reviewed heads. Every other source and test blob, including the 29 Product modules, Wanted, Pruned, BandPreparation and OrderGlue with its clients, equals its reviewed blob. Against main, the only removed lines are:

refactor(finset): use order-embedding names in OrderGlue #1554's reviewed OrderGlue renames, in OrderGlue.lean, Levels.lean, Batch.lean and Encoding.lean;
one UPSTREAM row, where main's OrderGlue follow-up row is replaced by refactor(finset): use order-embedding names in OrderGlue #1554's "refactor(finset): use order-embedding names in OrderGlue #1545 resolves…" row.

Docs intact.

NOTICE adds the pruned-evaluator and band-preparation credits.
ROADMAP.md adds separate bullets for the pruned evaluator (feat(wordram): execute sparse pruned tensor queries #1526), band preparation (feat(wordram): prepare thin-matrix bands and compose native encoders #1523), routing (feat(wordram): route and group wanted thin-product queries #1561) and queried products (feat(wordram): compose native queried thin-matrix products #1581), each with its reviewed text.
UPSTREAM.md adds the band, pruned, routing and product paragraphs and retains the refactor(wordram): consolidate square-root kernels and assess power specializations #1553 post-integration follow-up record, the leaf-order/canonical-word catalogue contract and the exec_*/topic-module notes.
Main's text is untouched except the OrderGlue row. That includes the feat(wordram): implement shared tensor encodings #1520 encoder text, the CSLib refactor(circuits): combine mass-production overhead estimates #1158 entry and the tail.
Checks: no markers, no undefined or duplicate link definitions, and no truncation.
Aggregate: 2788 unique sorted imports for 2788 modules.
Citation: [AlmanWilliams2026, Section 2] in OrderGlue.lean is retained.

Nit (non-blocking): the ROADMAP pruned-evaluator bullet still says that "Query grouping, band/tile composition … remain under #1394". Within this carrier those are now delivered by the routing and queried-product bullets directly below it. That sentence could be trimmed in a follow-up.

Limits: no local build. Hosted build and ci-checks were still pending when I checked, and this verdict depends on them passing. Whether to deliver the stack combined is a coordinator decision; this review covers only tree and content identity.

SamuelSchlesinger · 2026-10-29T11:38:09Z

Agent carrier integration review by /root/review_stack_integration: FINAL at 7da96e65cf2c352d08142bb5a7ea65098008d8cc, conditional on required CI. I reused the exact outside integration review and checked the combined-delivery plan. The accepted matrix-layer union exactly covers the 140 changed source/test paths; each retains its reviewed source or landed-main version. Delivering these bounded milestones through this carrier does not require separate ancestor landings. Their accepted work must still be verified on main before recording them as landed via this PR.

Cross-carrier evidence and the combined-CI condition cover compatibility with native carrier 7dc1b996. Both merge orders are clean and canonical; the new OrderGlue API introduces no removed-name callers in the native additions checked. Main's abstracts/renderer, source credit and explicit resource/follow-up records are preserved. ET catalogue adaptation, the fast ET backend and the full #1394 endpoint remain separate. No local build repeated.

SamuelSchlesinger · 2026-10-29T11:58:15Z

Landed on main as ee1ab6f. Full PR CI and merge-group CI passed. Post-landing inspection confirms all 140 accepted source/test paths and modes match the reviewed carrier; source credit is retained.

This delivers #1536, #1554, #1562 and #1576 through the combined-delivery plan. Their PRs will be closed as delivered here, rather than individually merged. The original criteria of #1523, #1545, #1526, #1561 and #1581 are satisfied. The broader #1394 objective, ET input adapter/fast backend and tracked API follow-ups remain open. AI-assisted coordinator verification; existing independent reviews are linked above.

…ib-community#1625) * 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 metadata fix replaces blanket exposure with explicit exposure of its two code definitions. All affected clients check with the public pure-specification lemmas. The deliberately interrupted e8 checkpoint is NOT used as an all-six claim. One overlapping MCP dependency setup had a transient Windows artifact lock; serial retries and final six are clean. Kernel clients tie actual initialized Runs/halt to exact physical output and caller sentinels. Native VM cases cover nonzero/zero products, duplicate/empty queries and dirty workspace above the source modulus. A direct compiler client loads27%8=3, increments/stores4 and preserves both adjacent sentinels. Concrete numerical width budget passes387/fails386; zero N fails the explicit thin premise. Pinned source: anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, 3sum-apsp/ThreeSumApsp/Sec2/Theorem5.lean61-67 (exact products),146-149 (sparse leaves). Local file equals the pinned Git blob; conclusion fragments checked verbatim. Finite mathematics/source credit is inherited. Compiler/controller/proofs here are original native work, not a source-Light semantics/count transfer. Abstract assessment: no own selected statements, models, catalogue or rendering change. No whole3SUM headline promotion. ROADMAP/UPSTREAM retain the #1394 gap. PUBLICATION LIMIT: #1615 landed DURING this audit via ee1ab6f08ac77b1404d19c0371b0b0ac7daaa915 (reviewed carrier7da96e65cf2c352d08142bb5a7ea65098008d8cc); main now includes later native/frontend additions. The five direct machine/arithmetic prerequisites and entire Schonhage supplier remain byte-identical. This exact validated candidate is preserved on its reviewed a8 parent for coordinator-directed current-main compatibility work before publication. No parent remote is changed. Fresh exact-whole-layer NONAUTHORING compiler/callee/API/resource review is still required and is owned by root. Existing supplier reviews do not approve the new compiler. No new PR, outside approval, merge or endpoint completion is claimed. Local reproducible records: .lake/codex-three-sum-continuation/callable-product/ summary.json,static-summary.json,source-identity.json,source-mapping.json, pr-body.md,audit-source.py and logs. Durable evidence is this commit description; the issue handoff links it. AI assistance: Codex implementation/self-review with Lean MCP; fresh nonauthoring and outside reviews remain pending. * refactor(WordRAM): align ArrayNormalize module name and admission prose Address optional review nits on PR1625 at fd1f2fce. Rename Normalize.lean to ArrayNormalize.lean with identical file bytes, migrate every consumer and the sorted canonical aggregate without a compatibility shim, say widths at least the threshold, and record that full VM cases use m0/N1 while general execution/resource proofs cover all valid geometry. Existing review6497681504 is already linked; the missing-record observation was a timing snapshot. Validation: serial targeted Lean MCP ArrayNormalize, WordRAMMemoryWindow and SchonhageCallable all clean. Exact moved-blob identity and comment-erased Lean token identity modulo module-import migration pass; public declaration statements/bodies/attributes and native program meaning are unchanged. Canonical source import order and removal of every old path verified. Full citation/simp hygiene, targeted repository doc-name/new-test checks (12 modules/2 tests), strict14 PR-body names and complete d010-to-final/staged/unstaged diff checks pass. No aggregate/import-generation/all-six run for this bounded delta. Original f5/f8 all-six and final fd1 hosted all-checks green run40879707895 remain scoped to those revisions; repaired head requires refreshed hosted CI before integration. Full compiler/source reviews reused; focused module/import/doc/test-comment delta review requested after push. No abstract/model/resource change or endpoint claim. Evidence .lake/codex-three-sum-continuation/callable-product/review-rename. AI assistance: Codex implemented the mechanical API/documentation repair; no self-approval, human approval or new full review is claimed. --------- Co-authored-by: Samuel Schlesinger <SamuelSchlesinger@users.noreply.github.com> Co-authored-by: Codex coordinator <codex@users.noreply.github.com> Co-authored-by: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>

…ds (cslib-community#1637) * 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 metadata fix replaces blanket exposure with explicit exposure of its two code definitions. All affected clients check with the public pure-specification lemmas. The deliberately interrupted e8 checkpoint is NOT used as an all-six claim. One overlapping MCP dependency setup had a transient Windows artifact lock; serial retries and final six are clean. Kernel clients tie actual initialized Runs/halt to exact physical output and caller sentinels. Native VM cases cover nonzero/zero products, duplicate/empty queries and dirty workspace above the source modulus. A direct compiler client loads27%8=3, increments/stores4 and preserves both adjacent sentinels. Concrete numerical width budget passes387/fails386; zero N fails the explicit thin premise. Pinned source: anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, 3sum-apsp/ThreeSumApsp/Sec2/Theorem5.lean61-67 (exact products),146-149 (sparse leaves). Local file equals the pinned Git blob; conclusion fragments checked verbatim. Finite mathematics/source credit is inherited. Compiler/controller/proofs here are original native work, not a source-Light semantics/count transfer. Abstract assessment: no own selected statements, models, catalogue or rendering change. No whole3SUM headline promotion. ROADMAP/UPSTREAM retain the #1394 gap. PUBLICATION LIMIT: #1615 landed DURING this audit via ee1ab6f08ac77b1404d19c0371b0b0ac7daaa915 (reviewed carrier7da96e65cf2c352d08142bb5a7ea65098008d8cc); main now includes later native/frontend additions. The five direct machine/arithmetic prerequisites and entire Schonhage supplier remain byte-identical. This exact validated candidate is preserved on its reviewed a8 parent for coordinator-directed current-main compatibility work before publication. No parent remote is changed. Fresh exact-whole-layer NONAUTHORING compiler/callee/API/resource review is still required and is owned by root. Existing supplier reviews do not approve the new compiler. No new PR, outside approval, merge or endpoint completion is claimed. Local reproducible records: .lake/codex-three-sum-continuation/callable-product/ summary.json,static-summary.json,source-identity.json,source-mapping.json, pr-body.md,audit-source.py and logs. Durable evidence is this commit description; the issue handoff links it. AI assistance: Codex implementation/self-review with Lean MCP; fresh nonauthoring and outside reviews remain pending. * refactor(WordRAM): align ArrayNormalize module name and admission prose Address optional review nits on PR1625 at fd1f2fce. Rename Normalize.lean to ArrayNormalize.lean with identical file bytes, migrate every consumer and the sorted canonical aggregate without a compatibility shim, say widths at least the threshold, and record that full VM cases use m0/N1 while general execution/resource proofs cover all valid geometry. Existing review6497681504 is already linked; the missing-record observation was a timing snapshot. Validation: serial targeted Lean MCP ArrayNormalize, WordRAMMemoryWindow and SchonhageCallable all clean. Exact moved-blob identity and comment-erased Lean token identity modulo module-import migration pass; public declaration statements/bodies/attributes and native program meaning are unchanged. Canonical source import order and removal of every old path verified. Full citation/simp hygiene, targeted repository doc-name/new-test checks (12 modules/2 tests), strict14 PR-body names and complete d010-to-final/staged/unstaged diff checks pass. No aggregate/import-generation/all-six run for this bounded delta. Original f5/f8 all-six and final fd1 hosted all-checks green run40879707895 remain scoped to those revisions; repaired head requires refreshed hosted CI before integration. Full compiler/source reviews reused; focused module/import/doc/test-comment delta review requested after push. No abstract/model/resource change or endpoint claim. Evidence .lake/codex-three-sum-continuation/callable-product/review-rename. AI assistance: Codex implemented the mechanical API/documentation repair; no self-approval, human approval or new full review is claimed. * feat(ExactTriangle): checkpoint actual record product composition Personal worker codex-three-sum-continuation-t3-3dda8289, issue1626, ordinary child from1625 repairce1062483; no ancestor remote edits. Implements fixed320-register actual record selector/log/header/copies/complete163-register callable bank, all readback separations from actual producer Output, raw01 identity, occurrence/query-cap sparse bound, native initialized producer→first-record consumer, same-y prefix Runs/chargedhalt/answers/frame, original positive logarithmic width and physical-width-independent polynomial prefix words/support. Generic caller consumes every occupied ordinal. Initialized fixed client selects ordinalzero and proves it exists; this is not an outer instance loop or aggregate ETsolver. PreparationInput.exec_input is the coordinator-authorized narrow API seam, reusing the existing derivation/private fits_at_width; public runs_input reuses it with unchanged statement/hypotheses/budget. No native producer/callee program or input definition changes. All own modules, modified producer module, and new native prefix/copy/admitted closed positive-depth initialized test have clean targeted Lean MCP diagnostics. Tests include actual second-record decode at m2,n16^18 and raw01 copy; the huge complete input family is kernel-checked symbolically, not VM-enumerated. SOURCE CHECKPOINT ONLY: canonical import generation, final all-six, full static/hygiene/source identity, PRmapping and required fresh nonauthoring review remain pending. Root owns sole aggregate/static slot; no such process was launched. Original #1394 ordinary3SUM1.9992, aggregate ET/outerloop/prime/parameter/backend/witness work remain open. No PR/review/approval/merge/watch. Credit retained; original native adaptation/composition by Erik Demaine with Codex AI assistance. * feat(ExactTriangle): validate initialized record product adapter Refs #1626. The full #1394 ordinary distinct-position 3SUM 1.9992 endpoint remains open. No PR is opened by this worker; fresh whole-layer nonauthoring review is pending coordinator arrangement. Validated source tree: 8f59a54c6de13459c0a85d86546b12fc12c5003c Pinned main base: 8569de69ef05751c7e39e2ddd99d24d49f6aa1ec Preserved source checkpoint: 8f46341d456f6e3651beb02aac898a22a34a9883 Normal main merge: 8612aff051db4590f15efcb02fa37deb2992f6f5. Only ROADMAP/UPSTREAM conflicted; complete landed prose is preserved. After the checkpoint the only own Lean deltas are canonical imports and terminal Header proof simplification. Native programs, public statements and supplier credit are preserved. Original native implementation: fixed 320 registers and <=132352 flat slots including halt, no width reads. Reads the real six-word record/heap, computes m using NatLog, copies raw X/Y and all interleaved query occurrences, and invokes the complete 163-register runtime-relocated callable bank. Copying keeps raw 0/1; the callee charges signed doubling once. No catalogue/win…

…-community#1661) * 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 metadata fix replaces blanket exposure with explicit exposure of its two code definitions. All affected clients check with the public pure-specification lemmas. The deliberately interrupted e8 checkpoint is NOT used as an all-six claim. One overlapping MCP dependency setup had a transient Windows artifact lock; serial retries and final six are clean. Kernel clients tie actual initialized Runs/halt to exact physical output and caller sentinels. Native VM cases cover nonzero/zero products, duplicate/empty queries and dirty workspace above the source modulus. A direct compiler client loads27%8=3, increments/stores4 and preserves both adjacent sentinels. Concrete numerical width budget passes387/fails386; zero N fails the explicit thin premise. Pinned source: anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, 3sum-apsp/ThreeSumApsp/Sec2/Theorem5.lean61-67 (exact products),146-149 (sparse leaves). Local file equals the pinned Git blob; conclusion fragments checked verbatim. Finite mathematics/source credit is inherited. Compiler/controller/proofs here are original native work, not a source-Light semantics/count transfer. Abstract assessment: no own selected statements, models, catalogue or rendering change. No whole3SUM headline promotion. ROADMAP/UPSTREAM retain the #1394 gap. PUBLICATION LIMIT: #1615 landed DURING this audit via ee1ab6f08ac77b1404d19c0371b0b0ac7daaa915 (reviewed carrier7da96e65cf2c352d08142bb5a7ea65098008d8cc); main now includes later native/frontend additions. The five direct machine/arithmetic prerequisites and entire Schonhage supplier remain byte-identical. This exact validated candidate is preserved on its reviewed a8 parent for coordinator-directed current-main compatibility work before publication. No parent remote is changed. Fresh exact-whole-layer NONAUTHORING compiler/callee/API/resource review is still required and is owned by root. Existing supplier reviews do not approve the new compiler. No new PR, outside approval, merge or endpoint completion is claimed. Local reproducible records: .lake/codex-three-sum-continuation/callable-product/ summary.json,static-summary.json,source-identity.json,source-mapping.json, pr-body.md,audit-source.py and logs. Durable evidence is this commit description; the issue handoff links it. AI assistance: Codex implementation/self-review with Lean MCP; fresh nonauthoring and outside reviews remain pending. * refactor(WordRAM): align ArrayNormalize module name and admission prose Address optional review nits on PR1625 at fd1f2fce. Rename Normalize.lean to ArrayNormalize.lean with identical file bytes, migrate every consumer and the sorted canonical aggregate without a compatibility shim, say widths at least the threshold, and record that full VM cases use m0/N1 while general execution/resource proofs cover all valid geometry. Existing review6497681504 is already linked; the missing-record observation was a timing snapshot. Validation: serial targeted Lean MCP ArrayNormalize, WordRAMMemoryWindow and SchonhageCallable all clean. Exact moved-blob identity and comment-erased Lean token identity modulo module-import migration pass; public declaration statements/bodies/attributes and native program meaning are unchanged. Canonical source import order and removal of every old path verified. Full citation/simp hygiene, targeted repository doc-name/new-test checks (12 modules/2 tests), strict14 PR-body names and complete d010-to-final/staged/unstaged diff checks pass. No aggregate/import-generation/all-six run for this bounded delta. Original f5/f8 all-six and final fd1 hosted all-checks green run40879707895 remain scoped to those revisions; repaired head requires refreshed hosted CI before integration. Full compiler/source reviews reused; focused module/import/doc/test-comment delta review requested after push. No abstract/model/resource change or endpoint claim. Evidence .lake/codex-three-sum-continuation/callable-product/review-rename. AI assistance: Codex implemented the mechanical API/documentation repair; no self-approval, human approval or new full review is claimed. * feat(ExactTriangle): checkpoint actual record product composition Personal worker codex-three-sum-continuation-t3-3dda8289, issue1626, ordinary child from1625 repairce1062483; no ancestor remote edits. Implements fixed320-register actual record selector/log/header/copies/complete163-register callable bank, all readback separations from actual producer Output, raw01 identity, occurrence/query-cap sparse bound, native initialized producer→first-record consumer, same-y prefix Runs/chargedhalt/answers/frame, original positive logarithmic width and physical-width-independent polynomial prefix words/support. Generic caller consumes every occupied ordinal. Initialized fixed client selects ordinalzero and proves it exists; this is not an outer instance loop or aggregate ETsolver. PreparationInput.exec_input is the coordinator-authorized narrow API seam, reusing the existing derivation/private fits_at_width; public runs_input reuses it with unchanged statement/hypotheses/budget. No native producer/callee program or input definition changes. All own modules, modified producer module, and new native prefix/copy/admitted closed positive-depth initialized test have clean targeted Lean MCP diagnostics. Tests include actual second-record decode at m2,n16^18 and raw01 copy; the huge complete input family is kernel-checked symbolically, not VM-enumerated. SOURCE CHECKPOINT ONLY: canonical import generation, final all-six, full static/hygiene/source identity, PRmapping and required fresh nonauthoring review remain pending. Root owns sole aggregate/static slot; no such process was launched. Original #1394 ordinary3SUM1.9992, aggregate ET/outerloop/prime/parameter/backend/witness work remain open. No PR/review/approval/merge/watch. Credit retained; original native adaptation/composition by Erik Demaine with Codex AI assistance. * feat(ExactTriangle): validate initialized record product adapter Refs #1626. The full #1394 ordinary distinct-position 3SUM 1.9992 endpoint remains open. No PR is opened by this worker; fresh whole-layer nonauthoring review is pending coordinator arrangement. Validated source tree: 8f59a54c6de13459c0a85d86546b12fc12c5003c Pinned main base: 8569de69ef05751c7e39e2ddd99d24d49f6aa1ec Preserved source checkpoint: 8f46341d456f6e3651beb02aac898a22a34a9883 Normal main merge: 8612aff051db4590f15efcb02fa37deb2992f6f5. Only ROADMAP/UPSTREAM conflicted; complete landed prose is preserved. After the checkpoint the only own Lean deltas are canonical imports and terminal Header proof simplification. Native programs, public statements and supplier credit are preserved. Original native implementation: fixed 320 registers and <=132352 flat slots including halt, no width reads. Reads the real six-word record/heap, computes m using NatLog, copies raw X/Y and all interleaved query occurrences, and invokes the complete 163-register runtime-relocated callable bank. Copying keeps raw 0/1; the callee charges signed doubling once. No catalogue/window snaps…

cslib-community#1700) * 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 metadata fix replaces blanket exposure with explicit exposure of its two code definitions. All affected clients check with the public pure-specification lemmas. The deliberately interrupted e8 checkpoint is NOT used as an all-six claim. One overlapping MCP dependency setup had a transient Windows artifact lock; serial retries and final six are clean. Kernel clients tie actual initialized Runs/halt to exact physical output and caller sentinels. Native VM cases cover nonzero/zero products, duplicate/empty queries and dirty workspace above the source modulus. A direct compiler client loads27%8=3, increments/stores4 and preserves both adjacent sentinels. Concrete numerical width budget passes387/fails386; zero N fails the explicit thin premise. Pinned source: anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, 3sum-apsp/ThreeSumApsp/Sec2/Theorem5.lean61-67 (exact products),146-149 (sparse leaves). Local file equals the pinned Git blob; conclusion fragments checked verbatim. Finite mathematics/source credit is inherited. Compiler/controller/proofs here are original native work, not a source-Light semantics/count transfer. Abstract assessment: no own selected statements, models, catalogue or rendering change. No whole3SUM headline promotion. ROADMAP/UPSTREAM retain the #1394 gap. PUBLICATION LIMIT: #1615 landed DURING this audit via ee1ab6f08ac77b1404d19c0371b0b0ac7daaa915 (reviewed carrier7da96e65cf2c352d08142bb5a7ea65098008d8cc); main now includes later native/frontend additions. The five direct machine/arithmetic prerequisites and entire Schonhage supplier remain byte-identical. This exact validated candidate is preserved on its reviewed a8 parent for coordinator-directed current-main compatibility work before publication. No parent remote is changed. Fresh exact-whole-layer NONAUTHORING compiler/callee/API/resource review is still required and is owned by root. Existing supplier reviews do not approve the new compiler. No new PR, outside approval, merge or endpoint completion is claimed. Local reproducible records: .lake/codex-three-sum-continuation/callable-product/ summary.json,static-summary.json,source-identity.json,source-mapping.json, pr-body.md,audit-source.py and logs. Durable evidence is this commit description; the issue handoff links it. AI assistance: Codex implementation/self-review with Lean MCP; fresh nonauthoring and outside reviews remain pending. * refactor(WordRAM): align ArrayNormalize module name and admission prose Address optional review nits on PR1625 at fd1f2fce. Rename Normalize.lean to ArrayNormalize.lean with identical file bytes, migrate every consumer and the sorted canonical aggregate without a compatibility shim, say widths at least the threshold, and record that full VM cases use m0/N1 while general execution/resource proofs cover all valid geometry. Existing review6497681504 is already linked; the missing-record observation was a timing snapshot. Validation: serial targeted Lean MCP ArrayNormalize, WordRAMMemoryWindow and SchonhageCallable all clean. Exact moved-blob identity and comment-erased Lean token identity modulo module-import migration pass; public declaration statements/bodies/attributes and native program meaning are unchanged. Canonical source import order and removal of every old path verified. Full citation/simp hygiene, targeted repository doc-name/new-test checks (12 modules/2 tests), strict14 PR-body names and complete d010-to-final/staged/unstaged diff checks pass. No aggregate/import-generation/all-six run for this bounded delta. Original f5/f8 all-six and final fd1 hosted all-checks green run40879707895 remain scoped to those revisions; repaired head requires refreshed hosted CI before integration. Full compiler/source reviews reused; focused module/import/doc/test-comment delta review requested after push. No abstract/model/resource change or endpoint claim. Evidence .lake/codex-three-sum-continuation/callable-product/review-rename. AI assistance: Codex implemented the mechanical API/documentation repair; no self-approval, human approval or new full review is claimed. * feat(ExactTriangle): checkpoint actual record product composition Personal worker codex-three-sum-continuation-t3-3dda8289, issue1626, ordinary child from1625 repairce1062483; no ancestor remote edits. Implements fixed320-register actual record selector/log/header/copies/complete163-register callable bank, all readback separations from actual producer Output, raw01 identity, occurrence/query-cap sparse bound, native initialized producer→first-record consumer, same-y prefix Runs/chargedhalt/answers/frame, original positive logarithmic width and physical-width-independent polynomial prefix words/support. Generic caller consumes every occupied ordinal. Initialized fixed client selects ordinalzero and proves it exists; this is not an outer instance loop or aggregate ETsolver. PreparationInput.exec_input is the coordinator-authorized narrow API seam, reusing the existing derivation/private fits_at_width; public runs_input reuses it with unchanged statement/hypotheses/budget. No native producer/callee program or input definition changes. All own modules, modified producer module, and new native prefix/copy/admitted closed positive-depth initialized test have clean targeted Lean MCP diagnostics. Tests include actual second-record decode at m2,n16^18 and raw01 copy; the huge complete input family is kernel-checked symbolically, not VM-enumerated. SOURCE CHECKPOINT ONLY: canonical import generation, final all-six, full static/hygiene/source identity, PRmapping and required fresh nonauthoring review remain pending. Root owns sole aggregate/static slot; no such process was launched. Original #1394 ordinary3SUM1.9992, aggregate ET/outerloop/prime/parameter/backend/witness work remain open. No PR/review/approval/merge/watch. Credit retained; original native adaptation/composition by Erik Demaine with Codex AI assistance. * feat(ExactTriangle): validate initialized record product adapter Refs #1626. The full #1394 ordinary distinct-position 3SUM 1.9992 endpoint remains open. No PR is opened by this worker; fresh whole-layer nonauthoring review is pending coordinator arrangement. Validated source tree: 8f59a54c6de13459c0a85d86546b12fc12c5003c Pinned main base: 8569de69ef05751c7e39e2ddd99d24d49f6aa1ec Preserved source checkpoint: 8f46341d456f6e3651beb02aac898a22a34a9883 Normal main merge: 8612aff051db4590f15efcb02fa37deb2992f6f5. Only ROADMAP/UPSTREAM conflicted; complete landed prose is preserved. After the checkpoint the only own Lean deltas are canonical imports and terminal Header proof simplification. Native programs, public statements and supplier credit are preserved. Original native implementation: fixed 320 registers and <=132352 flat slots including halt, no width reads. Reads the real six-word record/heap, computes m using NatLog, copies raw X/Y and all interleaved query occurrences, and invokes the complete 163-register runtime-relocated callable bank. Copying keeps raw 0/1; the callee charges signed doubling once. No catalogue/wind…

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

Merge commit '21a3641bd8d436fdb3138f0a74528913417c313e' into coordina…

0cba851

…tor/refresh-1536-landed21-20261029 # Conflicts: # NOTICE # ROADMAP.md # UPSTREAM.md

This was referenced Oct 29, 2026

feat(wordram): prepare and encode all shared matrix bands #1536

Closed

refactor(finset): use order-embedding names in OrderGlue #1554

Closed

feat(wordram): execute sparse pruned tensor queries #1562

Closed

SamuelSchlesinger changed the base branch from work/three-sum-native-wanted-routing-20261028 to main October 29, 2026 11:23

SamuelSchlesinger requested a review from chris-ai1 October 29, 2026 11:24

chris-ai1 mentioned this pull request Oct 29, 2026

feat(3sum): integrate native preprocessing and conditional host #1570

Merged

SamuelSchlesinger added this pull request to the merge queue Oct 29, 2026

Merged via the queue into main with commit ee1ab6f Oct 29, 2026
5 checks passed

chris-ai1 mentioned this pull request Oct 29, 2026

feat(ExactTriangle): connect prepared matrices to finite adjacency #1616

Merged

edemaine mentioned this pull request Oct 29, 2026

feat(WordRAM): compile memory windows for callable thin products #1625

Merged

Navigation Menu

Repository navigation

feat(Schonhage): execute native queried thin matrix products - #1615

feat(Schonhage): execute native queried thin matrix products#1615
SamuelSchlesinger merged 111 commits into
mainfrom
work/three-sum-native-queried-product-20261028

edemaine commented Oct 29, 2026 •

edited by SamuelSchlesinger

Loading

Uh oh!

chris-ai1 commented Oct 29, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

chris-ai1 commented Oct 29, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

edemaine commented Oct 29, 2026 • edited by SamuelSchlesinger Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Native result

Source and reuse

Validation and review

Uh oh!

chris-ai1 commented Oct 29, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

chris-ai1 commented Oct 29, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

edemaine commented Oct 29, 2026 •

edited by SamuelSchlesinger

Loading