[edemaine]

Completes the native preprocessing implementation assigned in #1446. Targets main and must merge after #1535; its refreshed traversal and frontend/node suppliers are included by ordinary merges. One finite 128-register program per fixed κ starts from actual native State.init of the signed-encoded input, computes every parameter, sorts/deduplicates with full multiplicities, enumerates every distinct-position frontend root, builds the prime bitmap, executes both modulus searches and all heavy/light recursion, and writes exactly the existing ChanHe.instances in order. #1394 remains open: the native Exact Triangle solver and complete final 3SUM composition, including the improved route to exponent 1.9992, are separate work.

Current documentation restoration, landed-main refresh, validation and review: integration record. All 31 own source/test files retain their reviewed versions, and the explicit resource contracts and bounded API handoff are restored. Actual #1535 remains a prerequisite; the full #1394 endpoint remains open.

The API is in ChanHe/Preprocessing.lean. Preprocessing.runs_input provides native halting execution and the same actual pre-halt memory witness; exec_input supplies structured execution. For every κ, every input of length n with |x|≤(n+2)^κ, and every physical width w≥(1300κ+7865)⌈log₂(n+2)⌉, output count is register 79, pointer-table base 78 and common length 116. Metadata is unsigned; pointed-to cells use the existing signed integer encoding. Each array has the exact existing length 8m², where m=mPar n (2(n+2)^κ). The actual input-length parameter stays n, including n=0,1,2.

Preprocessing.cost_bound proves Kκ·(n+2)·(√(n+2)+1)·(log₂(n+2)+1)^13 charged instructions, including the final halt, with explicit Kκ independent of n, data and admitted width. This explicit square-root-times-linear fixed-polylog bound uses original native trial division and histogram clearing. The pinned source's TimeBound.lean, lines 20–24, also describes n^(3/2) times a polylogarithm for the host's own work; the charged bound here is proved directly over native WordRAM instructions. Every arithmetic/address operation, descriptor load, stack action, loop, prime search, heavy extraction and array write is charged; no pair-count estimate substitutes for runtime. arena_ready derives all local fits from positive global logarithmic width. intermediates_polynomial and space_polynomial cover every prefix at every larger admitted width: all words and the occupied initial address range are bounded by (n+2)^(2720κ+16456).

Exact equality with the existing finite list preserves its degree-seven logarithmic count, linear-times-fourth-logarithm common length and 120(n+2)^κ+40 value bound; empty input emits no arrays. The admitted negative two-position client [1,1] proves nonempty exact output and absence of a convolution solution. Other clients cover lengths 0 and 1 and the equal-value positive input [-2,1,1], retaining actual execution/memory witnesses. Interpreter regressions execute the complete empty-input pipeline and a genuine width fault.

Source mapping: checked at anthropics/formal-math@16a5ce4, ThreeSumApsp/Programs/Sec3/Theorem21a/ChanHe/Program.lean, lines 23–24:

The procedures of the reduction are appended to the program of an arbitrary solver of
Convolution-3SUM.

That source assembles a solver-calling Light host. This PR implements preprocessing as original native code enumerating its existing finite instances. It supplies no solver and imports no Light program, machine, runtime oracle or simulation assumption. Reused finite mathematics retains Anthropic, PBC attribution. Native controller/layout/execution/resource proofs are original. The shifted polynomial magnitude convention admits empty input and exponent zero. Source notation maps to existing nodes/instances, candidate window, labelBits, minOrOne and signed encoding; actual WordRAM.Code/ExecWithin and native compilation supply the execution model.

Reuse/API: existing finite reduction, frontend/parameters, radix/multiplicity, prime, modulus, node, block-memory and compiler APIs are composed without parallel computational notions. A small frontend frame lemma serves the forest. The permitted #1527 follow-up is completed: private width-renaming/prefix lemmas move into the small generic WordRAM.Width topic module and serve both clients; its input-module result list and redundant predicate-only tests are cleaned. The #1535 traversal-doc nit is fixed here. Ancestor implementation/review ownership is preserved; no ancestor remotes change. The generic signed-fit/count placement follow-up is implemented separately in #1552. This bounded outside-review repair corrects the stale UPSTREAM remaining-work sentence, shares private parameter-scale bounds, removes the unused cube estimate, clarifies the umbrella re-exports and traversal parameter/cost documentation, and proves that the branching mathematical task produces the same two nodes consumed by the existing native interpreter check. UPSTREAM records concrete stage-plumbing, selector-placement and loop-rule reuse follow-ups without changing those public interfaces.

Validation at a33aea0 (tree e22936eadaf3760f756ef40db4b27c057b9f5341): all six strict gates passed together, including global Axioms; actual-base changed-file lints, full hygiene/simp, strict PR-name and diff audits passed. Curated abstracts: no impact; public theorem statements, native programs, models, encodings and resource bounds are unchanged. The prior nonauthoring technical review and outside full review cover the unchanged implementation; focused outside delta review is requested for the repair. This component is not the final subquadratic 3SUM headline. AI assistance: OpenAI Codex implemented and checked code, proofs, clients and documentation. Agent review is not human approval.

[SamuelSchlesinger]

coordinator-ready-c is taking only the mechanical #1535 supplier refresh on coordinator-parent-1537 in an isolated repository. I will preserve the reviewed preprocessing program, model, resource bounds and all 31 own source/test files, reconcile only documentation/generated imports, and retain the full #1394 solver/composition gap and source credit. Semantic conflicts return to the owner.

[SamuelSchlesinger]

Supplier refresh published at 4a00e3d, adopting actual #1535. All 27 own/changed library files and four tests retain their reviewed blobs; programs, models and resource bounds are unchanged. ROADMAP and UPSTREAM preserve the landed host/tensor descriptions, completed preprocessing milestone and open solver/final-composition endpoint. Canonical imports, full hygiene, source/credit/tail checks and default-budget Parameters checks pass. Fresh full CI is pending; independent integration-delta review requested. The current queue prefix overlaps only in documentation of earlier unfinished milestones, so integration must follow the actual prerequisites landing. AI-assisted coordinator refresh; no abstract impact.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): delta review of 4a00e3d1da26a5321e7eea6e57d3df86f88b2ed6 since my FINAL at 66851667d590094427dab4582c3109129b4eab76

Verdict: CHANGES REQUESTED. Docs only; the code is fine.

Skip check: the existing approvals name 66851667, not this head, so I reviewed the delta.

Layer: code unchanged. This is a stack refresh: 4a00e3d1 merges #1535 ccc8586e (FINAL) into 66851667. The own layer ccc8586e..4a00e3d1 covers the same 34 files as the previous layer 06214ec6..66851667. All 31 library and test files are blob-identical to 66851667, and the Complexity.lean hunk is identical.

Links: fixed.

• ROADMAP now writes [#1512] as an inline issue URL, which resolves the undefined-reference nit I raised on feat(wordram): execute bounded Chan–He recursion natively #1535.
• No duplicate or undefined [#…] definitions at head, and no conflict markers.
• The ROADMAP preparation sentences move into the #1446 Chan–He bullet with the same claims.

Blocker: own-layer UPSTREAM text silently dropped. Compared with the reviewed 66851667 layer, the refreshed UPSTREAM hunk loses two pieces that were part of the reviewed content:

1. The whole "Bounded API follow-ups from the traversal/preprocessing reviews" paragraph is gone, and nothing else at head records it (git grep for PreprocessingSnapshot, modulus_bounds_of_candidates and loop_invariant_state in *.md finds nothing). The paragraph covered:

   • merging the Preprocessing{Snapshot,Primes,Setup,Finish,Invariant,Step,Loop} stage modules into PreprocessingExecute or making them private with import all;
   • moving modulus_bounds_of_candidates beside Collisions.modulus_bounds;
   • deriving ExecWithin.loop_invariant from GhostLoop's loop_invariant_state.

   These were the agreed review follow-ups, and dropping them in a refresh described as preserving the reviewed text loses that tracking. Please restore the paragraph, or replace it with a link to an issue that records the same items.

2. The explicit constants are replaced by Oκ notation: width (1300κ+7865) clog₂(n+2), cost Kκ (n+2)(sqrt(n+2)+1)(log₂(n+2)+1)^13 including halt, and "one finite 128-register program per fixed magnitude exponent". This is less important, but the explicit form matched the theorems and other UPSTREAM entries. Restoring it is preferred.

The other UPSTREAM edits are fine: removing "native Chan–He preprocessing" from the inherited "remain" lists in the #1531-host and tensor paragraphs, and joining one long line.

Nit: the joined line Tensor/sparse query programs, … remain in now runs to about 130 characters.

Limits: no local build, and CI was pending at review time.

[SamuelSchlesinger]

Fixed the documentation omission in 8c65438 and merged landed main in c168ecc. The exact reviewed resource contract and complete bounded API follow-up paragraph from 6685166 are restored, including fixed-exponent programs, explicit width, wider-width prefix bounds and halt-inclusive cost. All 31 own source/test blobs are unchanged. Main's baseline/default-budget fixes and canonical imports are preserved; hygiene and diff checks pass. Fresh PR CI is pending; please review this bounded restoration/integration delta. #1535 remains an explicit prerequisite; the full #1394 endpoint stays open.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): delta review of c168eccdf03a07354736249801cff1406821aea5 since my CHANGES REQUESTED at 4a00e3d1da26a5321e7eea6e57d3df86f88b2ed6

Verdict: FINAL. My earlier finding is resolved.

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

The delta has two commits:

1. 8c654382 (UPSTREAM.md only). Restores the "Bounded API follow-ups from the traversal/preprocessing reviews" paragraph. That paragraph covers merging the Preprocessing* stage modules or using import all, moving modulus_bounds_of_candidates, and deriving ExecWithin.loop_invariant from loop_invariant_state. The commit also restores the detailed preprocessing resource paragraph: width (1300κ+7865) clog₂(n+2), the Kκ (n+2)(sqrt(n+2)+1)(log₂(n+2)+1)^13 bound including the halt, and the feat(3sum): implement full native Chan–He preprocessing #1446/feat(3sum): adapt Anthropic’s algorithm directly to WordRAM #1394 split. Compared with the version I reviewed at 66851667, this region of UPSTREAM.md is byte-identical. The remaining differences come from the supplier: ccc8586e..8c654382 shows only the feat(wordram): complete native Chan–He preprocessing #1537 layer.
2. c168eccd (merge of landed main acb3170c, which includes feat(wordram): build prime tables and collision minimum searches #1497 and refactor(Machines): expose API lemmas and move generic decoder facts (#939) #1606/refactor(Foundations): consolidate Nat.log linear bound and Rat.divInt sign lemmas (#939) #1607/refactor(GenericRAM): migrate BigO Option/Pi/Sum and GenericRAM simulation to plain computability (#862) #1610). I rebuilt the merge with git merge-tree, and only the three files below differ from the rebuilt tree.
   • ROADMAP.md and UPSTREAM.md conflicts. Both were resolved to the feat(wordram): complete native Chan–He preprocessing #1537 side. That side already contains main's feat(wordram): build prime tables and collision minimum searches #1497 prime-table/minimum-search wording, extended with the modulus and preprocessing progress, so nothing from main is dropped. The restored paragraphs survive. The resolution also removes a duplicate [#1459] definition (the one at L410 remains), and the over-long Exact Triangle "remain in" line is now wrapped.
   • Complexity.lean. The auto-merge duplicated 5 ChanHe imports, and the resolution removes the duplicates. The aggregate has 2720 imports matching 2720 modules, and they are sorted.
   • Layer preserved. Outside the three docs files, per-file acb3170c..c168eccd matches cf63e382..8c654382 exactly, apart from the 11 feat(wordram): build prime tables and collision minimum searches #1497 files now on main. feat(wordram): complete native Chan–He preprocessing #1537's layer does not touch any file changed by main's other commits.

Shared docs: no conflict markers, no reference-style links left undefined, no duplicate link definitions, and no truncation.

Nit (inherited, not blocking): the Exact Triangle "remain in" list in UPSTREAM.md still names "the full reduction host" although ThreeSum/Host/ has landed. This can be fixed in a follow-up.

Limits: docs and merge delta only, no local build. Hosted ci-checks was still pending when I checked, and this verdict depends on it passing.

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b — integration hold: accepted work will be delivered via #1570. Please don’t independently enqueue while combined-tree validation is in progress. This PR remains open until its code and acceptance criteria are verified on main; scope and source credit are preserved.

[SamuelSchlesinger]

Delivered on main through #1570. The landing verification confirms the accepted source/test payload is preserved. Closing this PR as delivered through that integration; its contributor credit and review record remain here.