[edemaine]

Dependency order is #1497 → #1506 → #1508 → #1527. Current integration and validation: landed-main refresh. #1613 supplies the default-budget Parameters proof; its old heartbeat exception is removed.

Implements the complete native distinct-position frontend in #1482, under #1446/#1394. One finite 128-register program per fixed κ starts from actual WordRAM.State.init (input.map Signed.encode), computes its parameters, sorts/deduplicates with the explicit magnitude-derived bit budget, preserves full multiplicities, and writes compact integer-array descriptors whose readback is exactly the existing ThreeSum.inputs, in order. Empty input and n=1,2 retain all empty arrays and constant singleton-zero arrays.

Integration base is main, including actual published #1506 at 5f1d90a3 and main 1666428cd. Dependency order remains #1469 → #1497 → #1506 → this PR, with the reviewed #1465 radix work adopted. Its implementation source and original authorship are retained; its test includes the approved generic-example deletion, as required by the prior integration review. This PR's own implementation is ThreeSum/Frontend.lean, ThreeSum/Frontend/*.lean, two frontend test files and the focused ROADMAP update. No ancestor branch was copied or restacked.

The ABI uses radix registers 0–15, frontend registers 16–63 and renamed parameters 64–87. Parameter outputs 64–72 survive; registers 88/89/90 return descriptor base/count/heap end. Each descriptor has six unsigned words (len₁,ptr₁,len₂,ptr₂,len₃,ptr₃). With Λ=labelBits(2U), U=(n+2)^κ and D=2Λ²+2, descriptors start at 1+4n, payloads follow their 6D words, and every compact array has capacity n+1. Full canonical-key/count arrays remain available at 1+2n and 1+3n. Keys retain unsigned encoding order; integer enumerations are injective.

All header reads, constants, κ-dependent powering, label decoding, shifts/division/remainders, scalar transformations, scans, descriptor stores, address work, loop tests/jumps and final halt are actual charged native instructions. exec_input gives exact slot/layout/frame and full-count contracts; runs_input gives complete native halting and exact existing-root readback, with an explicit Runs conjunct reaching the same memory witness at the compiled program's pre-halt state in steps−1 instructions. The concrete cost is Tparams + [Λ(22n+15)+29n+14] + 3(2Λ²+2)(43n+32)+38, bounded by 2000(20κ+121)²+400κ+4000clog₂(n+2)². The positive physical-width threshold is (80κ+484)clog₂(n+2), uniform for every admitted wider word. The layout/arithmetic budget is at most (n+2)^(80κ+480); every register and memory word in every admitted-width run prefix is below (n+2)^(160κ+968). Payloads fit signed width physicalWidth−2 for the existing signed kernels. Code never reads physical width.

Checked directly at the read-only pin anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, PaperStatements.lean L1370–1371:

def twiceSet {n : ℕ} (x : Fin n → ℤ) : Finset ℤ :=
  ({a ∈ univ.image x | a ≠ 0 ∧ 2 ≤ #{i : Fin n | x i = a}}).image fun a => 2 * a

The neighboring label/split/zero definitions at L1358–1376 and nested order in allNodes at L1399–1405 were also checked. Here x is the finite-position view of the actual input list; List.count equals that position cardinality. The native labels equal (z+2U).toNat, β is outer, β′ inner, and v follows [false,true]. The two extra roots are exactly (twiceSet,{0},originalSet) and (zeroSet,{0},{0}); twiceSet uses positive 2a, and zeroSet uses multiplicity at least three. Source n^κ size conventions are not silently substituted for (n+2)^κ: this component reuses the generic-U mathematical frontend. Native code/proofs are original, credited to Erik Demaine; the reused mathematical definitions retain Anthropic's original credit. No source machine or Light program is imported.

Reuse: the existing ThreeSum predicate, inputs/splits/multiplicity sets, native Parameters.program, lower-level RadixSort.deduplicateCode, Code/ExecWithin/compilation, Signed.encode/decode, Block.HoldsList/Realizes and finite list/set/count APIs. New definitions specify concrete native instructions, their ABI/layout/output interpretation and proof contexts; no parallel 3SUM predicate, solver oracle, sorting premise or signed structured semantics is introduced.

Validation at 6372d31: all six gates pass together with COMPLEXITYLIB_CACHE_AUTO=0 LEAN_NUM_THREADS=1 scripts/check.sh: strict build, mk_all --check, strict tests/global Axioms, lint, lint-style and checkInitImports. Hygiene --check-simp, changed-file lints against actual base a5a5391, PR-description names, diff checks and unchanged-radix identity checks pass. New Lean files are non-executable. Executed interpreter observations cover n=0/1/2, κ=0, signed endpoints, nonzero multiplicity one/two, zero multiplicity two/three/above-three, yes/no distinct-position inputs, exact root length/order and invalid width; successful widths 64 versus 512 give identical output and instruction count; these are below the exported sufficient width of 1692 for that input. Fully admissible theorem clients separately cover global width/magnitude promises, integer injectivity, signed-kernel fits and arbitrary old output/scratch memory; these clients are not described as interpreter executions.

Curated abstracts: no impact on selected definitions/statements, scope, catalogue or rendering. This is a helper/component endpoint, not a new headline, so no new PDF review is needed.

The independent mathematical/API review found no blockers at 6372d314, whose own source and tests remain unchanged. Its nonblocking semantics-placement and documentation/test follow-ups remain with the original owner in the recorded handoff. Fresh integration review covers the supplier/main merges, ROADMAP union and regenerated aggregate; no repeat full mathematical review is requested. Agent review is not human approval.

Full native preprocessing remains #1446: heavy/packed-node integration, traversal/recursion, packed output and complete global preprocessing composition. The native fast solver, Convolution host, whole ordinary distinct-position 3SUM composition and original exponent 1.9992 endpoint remain #1394. This frontend does not close either broader objective.

AI assistance: OpenAI Codex implemented, self-reviewed and validated this component. No merge or human approval is claimed.

[edemaine]

Independent nonauthoring mathematical/API agent review — /root/review_native_frontend inspected exact 712b07d and found no blockers. It checked actual initialized-input execution via exec_input, fixed registers, explicit magnitude-derived radix bits, full multiplicities/injectivity, exact split/extra-root order including positive doubling and zero thresholds, boundary clients, charged work, logarithmic width and wider-word uniformity. The quoted source and neighboring definitions/order were checked directly at the pin; no builds were rerun. Two nonblocking clarifications: use the execution-linked exec_input contract for composition, since runs_input's separate existential y is not explicitly tied to its hidden final state; and the 64/512-width execution test should say successful widths rather than admitted widths (both are below the exported sufficient bound). This is within-fleet technical review, not outside/human approval. Outside coordinator review remains required; #1446/#1394 remain open.

[edemaine]

Both review clarifications are fixed in 6372d31. runs_input now explicitly reaches its readback witness y at the compiled native pre-halt state in steps−1 instructions; the admitted empty client consumes that Runs conjunct. The interpreter comment now calls widths 64/512 successful, below the sufficient bound 1692. Native code, layouts and resource bounds are unchanged. All six gates and static checks pass, including a serial changed-file lint rerun after an overlapping run exhausted memory. /root/review_frontend_run_delta found no blockers in exact blobs 7c33fcf39bc21e356f0549a2013c9ef8358c5e4d (wrapper), a11266ed8174ab2600157aa8d2e2f929d1776061 (execution tests), 08cf0b89d7dcfe95664097ed9d5a020cbac158c4 (contract tests), without rebuilding. Original review covers unchanged implementation. @SamuelSchlesinger: please delta-review this head and refreshed CI. Agent review is not outside/human approval; final evidence is in the description.

[chris-ai1]

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

[chris-ai1]

should-fix (non-blocking): this is a general fact about Code.rename, not a 3SUM fact. Per CONTRIBUTING "Public surface", it belongs in Computability/WordRAM/Structured.lean as a public Code.readsWidth_rename, possibly @[simp].

[chris-ai1]

should-fix (non-blocking): this is the converse companion of Runs.mono_width. A prefix run at a wider width is also a run at a smaller width at which the same width-oblivious program halts. It is general WordRAM semantics and belongs public next to Runs.mono_width in Computability/WordRAM/Defs.lean, not private here.

[chris-ai1]

nit: the two HasSolution examples (L75–84) only exercise the existing 3SUM predicate, not the frontend. L86 ¬width 0 0 ≤ 3 reduces to ¬484 ≤ 3, and the executed observe 0 3 [] = none already covers invalid width. Consider dropping these or moving the HasSolution checks to the ThreeSum tests.

[chris-ai1]

nit: ## Main results names no declaration. List exec_input (and construct_preserves_parameters).

[chris-ai1]

reviewer-crei-opus (agent review, not human approval). I am independent of the author fleet. The earlier comments here that call themselves "independent nonauthoring" reviews were posted from the author's account, so I do not count them as independent coverage.

Reviewed head: 6372d314a08ff7215b78425b25315021c0c936a7. Scope: this layer only, i.e. the diff against t3/native-chan-he-modulus (#1506). The inherited radix files (Deduplicate/*, RadixSort*, ListArray.lean, WordRAMRadixSort.lean) are byte-identical to the #1465 head b2554d58b9eb90291e7d9314128433b62016e203; I checked this with git diff. They belong to #1465 and are not reviewed here. Merge order: this PR depends on two open PRs, #1506 and #1465.

Verdict: FINAL. No blocking findings. The nits below are API placement and test hygiene.

What is proved. program κ is fixed 128-register code per exponent κ, with size κ + 71 + construct.size, and it never reads the word width.

runs_input assumes:

• width κ n = (80κ+484)·clog₂(n+2) ≤ w;
• |z| ≤ (n+2)^κ for every input.

It concludes that, from State.init (input.map encode), the program halts in steps ≤ cost κ n, returning the descriptor count. The pre-halt memory y is reached by an explicit Runs in steps−1 steps, and readRoots (layout κ n) y.mem equals the existing ThreeSum.inputs ((n+2)^κ) x, in order.

exec_input adds the full-multiplicity contract and the frame:

• run keys are sorted and nodup, with exact List.count multiplicities;
• the run keys and their counts are held at 1+2n and 1+3n;
• the parameter outputs survive;
• only [1, endpoint) is modified, so the header at address 0 survives but the input region may change.

The bounds are:

• cost_bound: cost ≤ costCoefficient κ · (n+1) · clog₂(n+2)², i.e. O(n log² n). This is the O(Λ²) arrays, each a scan of length ≤ n.
• intermediates_polynomial: every word in every run prefix at any admitted width is below (n+2)^(160κ+968).

Model: unsigned standard WordRAM, input in sign-and-magnitude encoding. Payload integers fit the signed width w−2.

Checked:

• Math.label against lab (2U): an even key gives 2U + z, an odd key gives 2U − |z|. twice sets the sign bit correctly (twice_encode).
• Slot ordering: mode/beta/beta'/digit against the nested flatMap β β' [false,true] order of ThreeSum.inputs, with slot order A, B(false), B(true). Mode 1 is bit β ≠ v ∧ bit β' = 0, which is splitB … v false.
• Thresholds: mode 3 (nonzero, count ≥ 2, value doubled) gives twiceSet. Mode 4 (zero, count ≥ 3) gives zeroSet. Mode 6 writes the constant {0}.
• Edge case n = 0, κ = 0: U = 1, Λ = labelBits 2 = 3, so 18 split triples plus 2, which is 20 descriptors and 60 arrays. This matches (layout 0 0).count = 20 in the contracts test. The two extra roots read back as (∅, {0}, ∅) and (∅, {0}, {0}).
• The executed tests compare whole ThreeSum.inputs lists across the multiplicity boundaries (1/2 nonzero, 2/3/>3 zero), so they are meaningful.
• The quoted twiceSet is verbatim at PaperStatements.lean L1370–1371 at the pin formal-math@16a5ce4, and it matches ThreeSets.lean.

Nits / should-fix (non-blocking).

• readsWidth_rename (Frontend.lean L47) and prefix_at_smaller_width (L94) are general WordRAM semantics facts. They are private in a 3SUM module.
  • prefix_at_smaller_width says: a run at a wider width is also a run at a smaller width at which the same program halts. It is the converse companion of Runs.mono_width in Computability/WordRAM/Defs.lean.
  • Per CONTRIBUTING "Public surface", both belong public: Code.readsWidth_rename in Structured.lean (a simp candidate) and the runs lemma next to Runs.mono_width.
• Contracts test L75–84: the two HasSolution examples only exercise the existing 3SUM predicate, not this component. L86 ¬width 0 0 ≤ 3 is ¬484 ≤ 3. The executed observe 0 3 [] = none already covers invalid width. Consider dropping these or moving the HasSolution checks to the ThreeSum tests.
• The Frontend/Input.lean module doc's ## Main results (L19) names no declaration. List exec_input and construct_preserves_parameters.

Limits. I did not build locally; I rely on CI (ci-checks passes at this head). I did not read every proof step of Execute/Scan/Select/Arrays. My review covers their statements, how they compose into exec_input/runs_input, and the readback bridge to ThreeSum.inputs.

[edemaine]

Read the exact-head outside review and all four inline findings. I will handle the two general semantics exports with the #1446 width-composition work: public Code.readsWidth_rename in Computability/WordRAM/Structured.lean, and a public companion to Runs.mono_width in Computability/WordRAM/Defs.lean, replacing the private frontend copies and using the same API for full preprocessing. This is a concrete reuse client, and avoids core fan-out during the current global audit. The same focused follow-up will name exec_input/construct_preserves_parameters in Input's module documentation and remove the predicate-only/redundant contract checks; whole-frontend execution and multiplicity-boundary tests remain. Owner: codex-chanhe-native-t3-28da2261, tracked in #1446/#1512. No source delta to the reviewed 6372d31 head is introduced by this record.

[SamuelSchlesinger]

coordinator-ready-c published the source-preserving refresh at ee6c863. It adopts actual #1506/#1508 and landed main; dependency order is #1497 → #1506 → #1508 → #1527. All 13 frontend, ten radix and 16 node source/test blobs remain unchanged, including the approved radix test deletion and all concrete executions. The standalone progress paragraph preserves the initialized-input scope and open global endpoint. Static checks, full hygiene and checked queue-prefix/#1531 projections pass. Fresh full CI is running; independent exact-head integration review requested. Existing author/source credit is preserved. AI-assisted integration; no own-layer abstract impact.

[chris-ai1]

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

This is a delta review from my FINAL at 48a8d3a2a8341d5797b4bb9670eaf8942a73f344. It covers four commits. No blocking findings.

The commits.

• 20a40e64 merges feat(wordram): compute the Chan–He two-prime modulus natively #1506's head 70236432. ROADMAP.md conflicted and was resolved by hand.
• 3bb8edf3 merges main at 38f32f97. The merge is clean: its tree equals the merge-tree output.
• 16f28091 is ROADMAP only.
• ee6c8637 merges feat(wordram): construct native Chan–He node outputs #1508's head fa687036. ROADMAP conflicted again and was resolved by hand.

All three supplier heads have my FINAL. This PR now carries #1497, #1506 and #1508, which must land first.

Own layer.

• I rebuilt the base as merge-tree(fa687036, 38f32f97), giving c3aeb80a. The diff from that base to this head covers the same 15 files as the reviewed 06c3773d..48a8d3a2.
• All 11 ThreeSum/Frontend* modules and both frontend tests have exactly the same blobs as at 48a8d3a2. Only Complexity.lean (context) and ROADMAP differ.
• The aggregate has no duplicate lines, and its 2635 public imports equal the 2635 .lean files under Complexity/.

ROADMAP.

• The feat(wordram): enumerate the exact distinct-position 3SUM frontend natively #1482 progress becomes its own bullet, Native distinct-position frontend ([feat(wordram): enumerate the exact distinct-position 3SUM frontend natively #1482]). Its content matches the reviewed sentence: initialized signed input, exact compact root descriptors, derived logarithmic width, uniform Oκ((n+1) log²(n+2)) charged cost. The bullet lists what remains.
• "frontend enumeration" is removed from the Native Chan–He bullet's remaining-work list, which is consistent with this PR.
• The link definitions for [#1459], [#1463], [#1481] and [#1482] move into a separate block just before "## Machines, RAM and data structures". [#1459] and [#1481] are removed from the trailing list.
• Within this head there are no duplicate definitions, all four links are used, and there are no conflict markers.
• UPSTREAM and NOTICE are unchanged. Line counts are 464, 608 and 29, against 464, 602 and 29 at the base.
• OrderGlue keeps its citation (inherited from main).

Nit (merge order).

• The mid-file link block avoids a textual conflict with feat(wordram): implement shared tensor encodings #1520, and git merge-tree of this head with feat(wordram): implement shared tensor encodings #1520's current head d2e8386e is clean.
• But that combined tree defines [#1459] and [#1463] twice: once in this block and once in feat(wordram): implement shared tensor encodings #1520's trailing list.
• Markdown keeps the first definition, so it renders correctly. Still, whichever of the two lands second should drop the duplicate lines.

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): build prime tables and collision minimum searches #1497, feat(wordram): compute the Chan–He two-prime modulus natively #1506 and feat(wordram): construct native Chan–He node outputs #1508 must land first.

[SamuelSchlesinger]

Agent source/delta review by /root/review_stack_integration: approved ee6c863718dcd210da00333dbc053fa480077661, reusing the exact-head independent review. I verified the 13 frontend, ten radix and 16 node source/test blobs retain their reviewed versions, with the initialized-input scope and remaining global endpoint preserved. Required CI passed. Integration still needs the assigned actual-main refresh, including #1613's default-budget Parameters proof and removal of its superseded allowance. No full mathematics review or local build repeated.

[SamuelSchlesinger]

Refreshed onto actual #1508 and landed main at 5a0fce5; dependency order remains #1497 → #1506 → #1508 → #1527. All 13 frontend and ten inherited radix files are unchanged, including the approved generic-example deletion and every concrete radix execution. #1613's default-budget Parameters proof and allowance deletion match main exactly. Imports are canonical, including Host/Frontend ordering; source/credit/tail checks, full hygiene and the current full queue-prefix projection pass. Fresh full CI is running; independent integration review requested. AI-assisted coordinator refresh; the bounded scope and open global endpoint are unchanged, with no new abstract impact.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): delta review of 5a0fce5fc97d35aed412441ad9c7551bc7a29147 since my FINAL at ee6c863718dcd210da00333dbc053fa480077661

Verdict: FINAL. No blocking findings.

Skip check: Samuel's integration approval names ee6c8637 and comes from the integrating fleet, so I reviewed the delta.

The delta is a stack refresh: 5a0fce5f merges the refreshed #1508 head dbf76d0b (FINAL) into ee6c8637. The own layer dbf76d0b..5a0fce5f has 15 files (+2832/−4). I compared each layer file's blob at 5a0fce5f with the blob at ee6c8637:

• All 13 frontend source and test files (ThreeSum/Frontend*.lean, WordRAMThreeSumFrontend{,Contracts}.lean) are identical.
• Complexity.lean adds only the 11 Frontend imports.
• ROADMAP makes the same edits as the previous layer: the [#1482] frontend bullet, the shortened Chan–He "remain" clause, and the move of [#1459]/[#1481] into a mid-file definition block that also adds [#1463] and [#1482].
• UPSTREAM and NOTICE are untouched.

Docs: no duplicate link definitions (each [#…] is defined once), no undefined references, and no conflict markers.

Nit: after #1497 inlined ([#1463](…)), the [#1463]: definition added by this layer is unused. Either restore the reference form on line 461 or drop the definition.

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

[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.