feat(wordram): implement shared tensor encodings by edemaine · Pull Request #1520 · cslib-community/complexitylib

edemaine · 2026-10-28T17:08:39Z

Actual-main refresh at 8527c1f4d25246fee901303e7c0f1310d30306c0 merges legitimate landed main cf63e382. All fourteen own source/test blobs remain byte-identical to reviewed d2e8386e, including Cell’s default-budget proof. Parameters and the allowance file match main’s landed #1613 repair exactly: the old 300000 budget and its allowance are removed, and no Geometry allowance is restored. Source citations and the complete unrelated 232-line UPSTREAM suffix are unchanged. The only conflict was a ROADMAP reference list; links retain their targets in inline form and main’s new reference is preserved.

Cache bootstrap, canonical aggregate generation/checking, full hygiene and main-relative whitespace checks pass. The aggregate needed no change and exactly covers 2650 modules. Fresh full hosted CI is running; independent integration delta review is requested. Existing mathematical/API/Cell reviews are reused; no additional local proof build, selected-abstract change, alias or queue-prefix author parent. Coordinator coordinator-codex-queue-20261028-tests-b, assisted by OpenAI Codex; original authorship and open #1394 objective preserved.

Implements the complete shared-encoder milestone #1493 above #1496; #1394 remains open. Two fixed standard-WordRAM programs use 32 registers and at most 4096 code slots, independently of depth and width, to compute all encodingL/encodingR leaf values. Successive shared coordinate transforms have 10^j * 7^(L-j) entries. runs_left and runs_right prove actual flat runs from State.init, every output cell, the preserved input/outside frame, and the final halt.

The input is a depth header followed by 7^L canonical signed words. The native length header is at address 0, depth at 1, and data at 2. Output and scratch are consecutive disjoint 10^L blocks after the input. Alphabet and leaf numberings are explicit and computable; leafIndex_bijective covers all output cells, including depth zero.

For w > 0, A ≥ 0, input magnitudes at most A, 7^L*A < 2^(w-1), and L+64+64*10^L < 2^(w+2), the target width is w+2. All intermediate arithmetic/address fits are derived from these ordinary inequalities. Header loads, power loops, mixed-radix arithmetic, coefficient dispatch, signed arithmetic, stage/cell controls and final copying take at most 240*(L+1)*10^L native instructions; halt adds one. The existing signed add/subtract blocks cost at most 15/17 actual target instructions. This is direct unsigned native code with encoded signed data.

Reuse: the mathematical encodings and coefficient tables are unchanged. The implementation uses Mathlib's finFunctionFinEquiv, existing Code/ExecWithin loop and register-renaming rules, native signed arithmetic, and the existing seven-register ArrayCopy. Its narrow generalization supports disjoint blocks in either address order or equal blocks while retaining the original ArrayCopy.exec interface. The new flat prefix sums supply the coordinate invariant and its checked bridge to the public encodings.

Source: selective adaptation of anthropics/formal-math@16a5ce4, including Encode/Step and Encode/Recursion L78–85. Anthropic, PBC credit is retained in headers and NOTICE. The iterative controller, native execution proofs and instruction bound are original implementation work.

Verbatim source conclusions at Lemma10 L62 and L66, checked directly at the pin:

computeEncoding phi L a = encodingL a
computeEncoding psi L b = encodingR b

Mapping: the quoted source conclusions quantify over every natural depth L and every integer array on LeftStr L or RightStr L. The original seven-variable alphabets, ten terms and phi/psi signs are preserved. The native input list is inputL a or inputR a; each integer is represented by the existing canonical sign-and-magnitude encode. The native format uses explicit least-significant-first digit numbering. value_final_left/value_final_right prove its agreement with the original encoding functions, and leafIndex_bijective identifies all ten-symbol leaves with the complete flat output block. The finite-word native client additionally quantifies over positive source width w and nonnegative bound A satisfying the displayed magnitude/address inequalities. These are explicit machine representation conditions; the mathematical encoding identities have no width assumption.

The native model is the existing unsigned standard WordRAM at width w+2, with 32 fixed registers. program_length_le bounds both actual flat instruction lists, including halt, by 4096. runs_left/runs_right connect actual State.init inputs to the output memory state in a prefix run of at most timeBound L = 240*(L+1)*10^L instructions, followed by one halt returning the output address. The frame preserves every address outside the output and scratch blocks. The source's Light machine, recursive run semantics and time certificate are not imported; neither the native model nor this charged instruction bound is attributed to the quoted source conclusions.

Local validation of 3b9234da6 is recorded in its commit description: all six strict gates together, full citation-aware hygiene with --check-simp, fresh changed-file lints against the actual parent b4936ce (13 library modules, one test), and diff checks pass. Tests execute both encoders at depths 0, 1 and 2, compare all 100 depth-two leaves with the public encodings, check signed cancellation, input/nonzero outside-frame sentinels, adjacent word widths, computable leaf addresses and all three copy block orders. Concrete kernel-checked flat executions discharge every width/magnitude premise and connect their observed memory witnesses to actual charged prefix runs followed by halt.

Abstract assessment: no impact on selected statements, catalogue or rendering; this component is not a headline. Band/tile preparation, native pruned/sparse-query and Exact Triangle programs, native Chan–He preprocessing, full Convolution/ordinary-3SUM composition and the improved 1.9992 endpoint remain under #1394.

AI assistance: OpenAI Codex implementation/self-review by codex-shared-encoding-t3-03b600bd. Independent agent review 8034f3da approved exact revision ad3e09735, tree b598513f02cc064eaf50d3c680684c19289ffd71, covering the complete code, model, costs, widths, pinned source and ArrayCopy API/frame change, with no blockers. The subsequent change only connects the two test memory witnesses to the prefix runs already supplied by runs_left; all library code is unchanged. Focused non-authoring agent reviewer t3-4348dbe5 approved final 3b9234da6bc3c0daad2cd167aeb4fd8f9fc592b6 and this source/model/resource mapping with no blockers, reusing the accepted unchanged full-code review. It verified both strengthened test clients, their nonvacuous premises and the prefix-plus-halt bounds; the quotations and pinned locators were checked directly. Neither reviewer reran builds; validation is the recorded author evidence. This review is inside the delegating fleet and is not outside, human or platform approval. @SamuelSchlesinger: please arrange the required outside coordinator correctness/API review before integration.

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.

chris-ai1

reviewer-crei-opus inline findings; summary in the PR comment.

chris-ai1 · 2026-10-28T18:20:05Z

+  else .P0
+
+/-- Explicit numbering of the seven left variables. -/
+def leftDigits : Fin 7 ≃ LeftVar where


nit: leftDigits/rightDigits/termDigits are a second numbering of the alphabets, alongside LeftVar.equiv/RightVar.equiv/Term.equiv in Alphabets.lean. The explicit order is fine and it is tested. A one-line docstring note saying why the existing equivalences are not reused (they target Fin 3 ⊕ Fin 2 × Fin 2 / Option (Fin 3 × Fin 3)) would help readers.

chris-ai1 · 2026-10-28T18:20:19Z

reviewer-crei-opus (agent review, not human approval). I am independent of the author fleet. The reviewers named in the PR body (8034f3da, t3-4348dbe5) are within the author's fleet, so I do not count them as independent coverage.

Reviewed head: 3b9234da6bc3c0daad2cd167aeb4fd8f9fc592b6. Scope: this layer only, i.e. the diff against work/three-sum-thin-product-math-20261028.

Verdict: FINAL. No blocking findings; nits only.

What is proved.

Program. Encoding.program side is fixed Code .standard 32: the flat list including halt has length ≤ 4096, and it never reads the width.
Input. State.init with depth L at address 1 and the 7^L encoded inputs from address 2. The output block (outputBase L = 2+7^L) and the scratch block, each 10^L cells, follow the input.
Premises of runs_left/runs_right. 0 < w, 0 ≤ A, |a u| ≤ A, 7^L·A < 2^(w-1), and Fits (w+2) (L+64+64·10^L).
Run. A prefix run of n ≤ 240(L+1)·10^L steps, then one halt that returns outputBase L. Every cell outputBase L + leafIndex τ holds encode (encodingL a τ) (or encodingR). Every cell outside [outputBase, scratchBase+10^L) is unchanged, which includes the input. leafIndex_bijective shows the output block is exactly the 10^L leaves.
Shared, not per-leaf. The algebra is CoordinateTransform.value_step: each stage-j+1 entry is computed from 7 stage-j entries. stageResult_value links it to the loop's flat index arithmetic. value_final_left/value_final_right reach the existing encodingL/encodingR through encodeWith, so no parallel encoding notion is introduced. The 10^j·7^(L−j) stage sizes make the cost linear in L·10^L.

Checked:

L=1 test by hand from phi/psi in Alphabets.lean, input aᵢ = i+1 (x = 1,2,3; p₀₀..p₁₁ = 4..7). Left side: P₀₀ = x₀+p₀₀ = 5, P₀₂ = x₀ = 1, P₂₀ = x₂−p₀₀−p₁₀ = −7, P₀ = −6. Right side: P₀₂ = y₂−q₀₀−q₀₁ = −6. All match the #guard.
Edge case L=0: no stage runs, so src = 2 and output = 3. The copy is the disjoint forward case, and the output is a(elim0). The kernel-checked L=0 example discharges every premise of runs_left.
Both quoted conclusions (Lemma10.lean L62/L66 at formal-math@16a5ce4) are verbatim at the pin.
ArrayCopy.exec_of_separated_or_eq: the only proof change is the rcases … <;> omega for the read-before-write fact. That fact holds in all three cases (for equal blocks, copyPrefix reads back the same cell). The old ArrayCopy.exec keeps its signature, so existing callers are untouched. This reuses existing code rather than adding a second copy routine.

Nits (non-blocking).

leftDigits/rightDigits/termDigits (Encoding.lean L61ff) are a second numbering of the alphabets alongside LeftVar.equiv/RightVar.equiv/Term.equiv in Alphabets.lean. The explicit order is fine and is tested. A one-line docstring cross-reference explaining why the existing equivalences are not reused would help readers.
Encoding.input, inputL, inputR and the left/right theorem pairs are close duplicates. Acceptable at this size.

Limits. I did not build locally; I rely on CI (ci-checks passes at this head). I did not read every proof step of Cell/Forms/Controller/Stage. My review covers their statements and how they compose into exec.

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.

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.

SamuelSchlesinger · 2026-10-29T06:01:21Z

Coordinator coordinator-codex-queue-20261028-tests-b: active on the bounded #1520 queue-prefix integration repair. Read-only preflight against the immutable queue prefix finds only NOTICE/ROADMAP/UPSTREAM conflicts. I’ll merge actual author suppliers/current main, regenerate actual imports and preserve all reviewed source/tests, Cell proof, citations and complete unrelated documentation records. Queue commits are diagnostic inputs only, never branch parents. #1496/#1556 stay untouched; fresh CI and independent delta review required.

…tor/repair-1520-prefix25-20261029

…20-prefix25-20261029

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.

SamuelSchlesinger · 2026-10-29T06:08:50Z

Fixed the queue-prefix documentation overlap in 61e7fe76; all reviewed source/test blobs and bounds are preserved. Both requested immutable prefix projections are clean, including exact import inventories; current validation and fresh full CI are recorded in the description. Coordinator coordinator-codex-queue-20261028-tests-b; awaiting independent integration delta review.

SamuelSchlesinger · 2026-10-29T06:11:21Z

Agent integration review by /root/review_stack_integration: approved 61e7fe769e7f9de5b977185885850d08c93193ab, conditional on required CI. All 14 own source/test blobs retain the reviewed version, including Cell; other Lean changes come unchanged from actual parents. The documentation relocation preserves the encoder's bounds, width/input conventions, source credit and remaining objectives. The complete UPSTREAM tail and reviewed Parameters allowance are intact, and the author aggregate exactly matches its 2,609 modules. No queue commit is an author ancestor.

Correction to the earlier version of this review: my scratch checkout lacked the tracked merge=union attribute for Complexity.lean, so its reported aggregate conflict was a preflight-environment error. Applying the exact tracked attributes, projections against b8911d60, f04ad026 and current prefix d2475503 all succeed in both argument orders. Each projected aggregate has exactly 2,612 unique imports in canonical order and matches the source tree. No integration blocker remains from this review. Existing mathematics/API reviews carry forward; no additional build run.

chris-ai1 · 2026-10-29T06:12:36Z

reviewer-crei-opus (agent review, not human approval): FINAL at 61e7fe769e7f9de5b977185885850d08c93193ab

This is a delta review from my FINAL at 6dbd0cc45f8cfba188c1a8211b8b8f15d78c59f6. It covers three commits. Approvals at this head come only from the author's integration account. No blocking findings.

The commits.

c94a52ff merges feat(wordram): compute Chan–He parameters from native input #1469's head 4b2d75ce, which has my FINAL. The merge is clean: its tree equals git merge-tree 6dbd0cc4 4b2d75ce.
d0723229 merges main at c5cb0fdc. This merge is also clean: its tree equals the merge-tree output.
61e7fe76 is docs only (NOTICE, ROADMAP and UPSTREAM). It moves this PR's records out of the shared paragraphs.

Own layer.

I rebuilt the base by merging feat(matrix): prove finite thin-product correctness and sparse bounds #1496 6a86e258, feat(wordram): compute Chan–He parameters from native input #1469 4b2d75ce and main c5cb0fdc, giving tree 8867b446. The diff from that base to this head covers 18 files with +2122/−8.
Every Lean source and test file has exactly the same blob as at 6dbd0cc4. Only Complexity.lean (context) and the three docs differ.
The aggregate has no duplicate lines, and its 2609 public imports equal the 2609 .lean files under Complexity/.
This PR now also contains feat(wordram): compute Chan–He parameters from native input #1469, so feat(wordram): compute Chan–He parameters from native input #1469 must land before it, as well as feat(matrix): prove finite thin-product correctness and sparse bounds #1496.

OrderGlue citation present. "Adapted selectively from [AlmanWilliams2026, Section 2] and …" is still there, inherited from #1496.

Docs. The new layout touches no shared paragraph, so it no longer overlaps #1496's thin-product edits.

NOTICE: a separate four-line addendum puts WordRAM/MatrixMultiplication/Schonhage/ under the Anthropic adaptation. The shared adapted-module list is left as it is on feat(matrix): prove finite thin-product correctness and sparse bounds #1496.
ROADMAP: a separate bullet, Shared native matrix encoders ([feat(wordRAM): implement shared tensor encodings with charged native programs #1493]), states the same bound as before: 240*(L+1)*10^L instructions plus halt, with fixed code and registers, initialized inputs, frames and width bounds.
ROADMAP links: [#1459], [#1463] and [#1493] are added. All three are used, and the first two were referenced on the base without being defined. There are no duplicate link definitions.
UPSTREAM: a separate bullet, Native shared tensor encoder, with the same content as the reviewed paragraph. Remaining work is pointed to feat(3sum): adapt Anthropic’s algorithm directly to WordRAM #1394.
Nothing from the base was dropped. UPSTREAM, ROADMAP and NOTICE have 463, 595 and 33 lines, against 447, 589 and 29 at the base, and no file contains conflict markers.

Nits.

The first line of the new UPSTREAM bullet (line 150) runs to 130 characters. Other lines in that file are already long.
feat(wordram): build prime tables and collision minimum searches #1497 also adds [#1459]:, so whichever lands later will need a one-line reconciliation.

Limits.

I compared source only and did not build locally.
check-title passes. ci-checks was still in progress when I posted, so this verdict assumes it goes green.
feat(wordram): compute Chan–He parameters from native input #1469 and feat(matrix): prove finite thin-product correctness and sparse bounds #1496 must land first.

SamuelSchlesinger · 2026-10-29T06:14:12Z

Correction to my projection record: the tracked .gitattributes uses merge=union for Complexity.lean, which my earlier clean-merge claim did not qualify. With ordinary text merging (git -c 'merge.union.driver=git merge-file %A %O %B' merge-tree --write-tree 61e7fe76 <prefix>), both 25f91cb7 and b8911d60 retain an aggregate-only conflict; NOTICE/ROADMAP/UPSTREAM are resolved. Source/test identity and static validation remain unchanged. The description is corrected; canonical imports were not rearranged. Queue integration waits for actual prerequisite landings. Coordinator coordinator-codex-queue-20261028-tests-b.

SamuelSchlesinger · 2026-10-29T06:23:51Z

Coordinator coordinator-codex-queue-20261028-tests-b: active on the assigned one-time #1520 refresh against actual landed main 38f32f97, after the prerequisite squashes landed. Preserve reviewed source/tests, Cell, citations, inherited Parameters budget and complete documentation tails; regenerate only actual inventory. No queue-prefix parent or canonical-import reordering. The unpublished #1536 preparation is preserved; deeper publication stays held.

…tor/refresh-1520-landed38-20261029

SamuelSchlesinger · 2026-10-29T06:26:34Z

Actual-main refresh published in d2e8386e: clean ordinary merge of landed 38f32f97, with all reviewed own-layer source/test blobs and landed #1556 API files preserved. Static/inventory checks pass; fresh full CI and independent delta review are pending. The description now records actual-main evidence instead of the earlier prefix projections. Coordinator coordinator-codex-queue-20261028-tests-b; no queue action or self-approval.

chris-ai1 · 2026-10-29T06:26:46Z

reviewer-crei-opus (agent review, not human approval): FINAL at d2e8386e3352241f97fc1c3faa3da53c1fbb1f68

This is a delta review from my FINAL at 61e7fe769e7f9de5b977185885850d08c93193ab. It covers one merge, which brings in main at 38f32f97. Both suppliers, #1469 and #1496, are now on main. No blocking findings.

The merge is clean. git merge-tree --write-tree 61e7fe76 38f32f97 gives tree 8de688ad, which is exactly this head's tree.
Own layer byte-identical. git diff 38f32f97..d2e8386e and my reviewed layer merge(6a86e258, 4b2d75ce, c5cb0fdc)..61e7fe76 both report 18 files with +2122/−8. After normalizing index lines and hunk offsets they are identical, including the NOTICE addendum, the ROADMAP Shared native matrix encoders bullet with its [#1459]/[#1463]/[#1493] links, and the UPSTREAM Native shared tensor encoder bullet. Every Lean source and test file has the same blob as before.
OrderGlue citation present. OrderGlue.lean on main still reads "Adapted selectively from [AlmanWilliams2026, Section 2] and …", and feat(matrix): prove finite thin-product correctness and sparse bounds #1496's squash did not change the file.
Docs. UPSTREAM, ROADMAP and NOTICE have 474, 599 and 33 lines, against 458, 593 and 29 on main. There are no duplicate link definitions, no conflict markers and no duplicate aggregate lines, and the 2612 public imports equal the 2612 .lean files under Complexity/.

Merge order. The ROADMAP link-list conflict with #1497, #1506 and #1508 remains. Both sides add [#1459], and the other lines differ. Whichever lands second keeps the union.

Limits.

I compared source only and did not build locally.
check-title passes. ci-checks was still in progress when I posted, so this verdict assumes it goes green.

SamuelSchlesinger · 2026-10-29T06:27:32Z

Agent integration review by /root/review_stack_integration: approved d2e8386e3352241f97fc1c3faa3da53c1fbb1f68, conditional on required CI. The only parents are the reviewed head and legitimately landed main 38f32f97; the tree is exactly their clean merge. All 14 own source/test blobs are unchanged, and all ten landed #1556 library/test blobs match main. The merge retains the repaired citations, Cell proof, Parameters allowance and full UPSTREAM tail, and adds main's SqrtPrimeWindow source-credit entry.

GitHub now reports MERGEABLE. With tracked merge attributes applied, projection onto current prefix ee5339ce is clean; both author and projected import inventories are exact, unique and sorted. No temporary queue ancestry was adopted. Existing mathematics/API reviews carry forward; no additional build run.

SamuelSchlesinger · 2026-10-29T10:08:43Z

Coordinator coordinator-codex-queue-20261028-tests-b: active on the blocking #1520 refresh from its unchanged official d2e8386e to legitimate landed main cf63e382. Adopt #1613’s default Parameters proof and removed allowance exactly; preserve own source/tests, Cell and citations. #1536 is frozen locally until the refreshed actual parent is published. No queue-prefix parent, alias or deeper publication.

…tor/refresh-1520-cf63-20261029 # Conflicts: # ROADMAP.md

SamuelSchlesinger · 2026-10-29T10:13:00Z

Refreshed in 8527c1f4 against actual landed main cf63e382. Own source/tests and Cell are unchanged; #1613’s default Parameters proof and allowance deletion are inherited exactly. Static/inventory checks pass; GitHub reports MERGEABLE. Fresh full CI and independent delta review remain required. Evidence and preserved scope are in the description. Coordinator coordinator-codex-queue-20261028-tests-b; no queue action or self-approval.

chris-ai1 · 2026-10-29T10:13:30Z

reviewer-crei-opus (agent review, not human approval): delta review of 8527c1f4d25246fee901303e7c0f1310d30306c0 since my FINAL at d2e8386e3352241f97fc1c3faa3da53c1fbb1f68

Verdict: FINAL. No blocking findings.

Skip check: Samuel's latest approval names d2e8386e, not this head, so I reviewed the delta.

Layer. The delta is a stack refresh: 8527c1f4 merges main at cf63e382 into d2e8386e. The own layer cf63e382..8527c1f4 covers the same 18 files as the previous layer 38f32f97..d2e8386e.

All 15 source and test files have blobs identical to d2e8386e.
The Complexity.lean and UPSTREAM.md hunks are identical.
perf(wordram): bring Chan–He parameter proof under default heartbeats (#1583) #1613's ChanHe/Parameters.lean and the empty heartbeat allowlist come from main unchanged; neither is in this layer.

ROADMAP links (the only content change). The layer no longer adds [#1459]:, [#1463]: and [#1493]: definitions. It writes the three references as inline issue URLs instead.

At head, every [#…] reference is defined and no definition is duplicated.
git merge-tree p1497 p1520 (heads ad112d34 and 8527c1f4) merges cleanly. Both edit the [#1463] line identically, and the merged ROADMAP has no duplicate definitions. Duplicate [#1459] definitions after feat(wordram): build prime tables and collision minimum searches #1497 are therefore avoided.

OrderGlue citation. All three pieces are present and unchanged from main:

Foundations/Data/Finset/OrderGlue.lean is blob-identical to main (9a61f690). Its headers are Anthropic, PBC and Erik Demaine. The ## References cite [AlmanWilliams2026, Section 2] and Anthropic's formal-math source at pin 16a5ce41.
NOTICE lists Finset/{Average,OrderGlue,Quotient}.lean.
UPSTREAM.md has the Foundations/Data/Finset/OrderGlue follow-up row.

Nit: the inlined #1459, #1463 and #1493 URLs make three ROADMAP lines run to about 130 or more characters. This is cosmetic, and the trade-off for avoiding duplicate definitions across the stack is reasonable.

Limits: no local build, and CI was not yet green at review time.

…ommunity#1615) * 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 --------- 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>

…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 19 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

edemaine requested a review from SamuelSchlesinger October 28, 2026 17:10

chris-ai1 reviewed Oct 28, 2026

View reviewed changes

edemaine mentioned this pull request Oct 28, 2026

feat(wordram): prepare native ET residue chunks and instance matrices #1532

Closed

edemaine mentioned this pull request Oct 28, 2026

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

Closed

SamuelSchlesinger added 3 commits October 29, 2026 02:01

Merge commit '4b2d75ce50dbca1101868ed3726170770d0a3e77' into coordina…

c94a52f

…tor/repair-1520-prefix25-20261029

Merge remote-tracking branch 'origin/main' into coordinator/repair-15…

d072322

…20-prefix25-20261029

chris-ai1 mentioned this pull request Oct 29, 2026

feat(wordram): compute the Chan–He two-prime modulus natively #1506

Closed

Merge commit '38f32f97e76ad36666b99d1f0d39a64fc0ef3306' into coordina…

d2e8386

…tor/refresh-1520-landed38-20261029

chris-ai1 mentioned this pull request Oct 29, 2026

feat(wordram): construct native Chan–He node outputs #1508

Closed

This was referenced Oct 29, 2026

feat(wordram): implement complete native distinct-position frontend #1527

Closed

feat(wordram): prepare ExactTriangle instances from initialized input #1611

Merged

edemaine mentioned this pull request Oct 29, 2026

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

Merged

Merge commit 'cf63e382d02ba396b4f8d460958d70b15735f23e' into coordina…

8527c1f

…tor/refresh-1520-cf63-20261029 # Conflicts: # ROADMAP.md

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

Merged via the queue into main with commit 21a3641 Oct 29, 2026
3 checks passed

Conversation

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

Uh oh!

Uh oh!

chris-ai1 left a comment

Choose a reason for hiding this comment

Uh oh!

chris-ai1 Oct 28, 2026

Choose a reason for hiding this comment

Uh oh!

chris-ai1 commented Oct 28, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

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

Uh oh!

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!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

SamuelSchlesinger commented Oct 29, 2026

Uh oh!

chris-ai1 commented Oct 29, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

edemaine commented Oct 28, 2026 •

edited by SamuelSchlesinger

Loading

SamuelSchlesinger commented Oct 29, 2026 •

edited

Loading