[edemaine]

Part of #1446; closes #1501 after integration. Targets main and must merge after #1497; its refreshed supplier and current main are included. This completes native two-prime modulus selection for three supplied integer arrays and a shared prime table, while full preprocessing and the #1394 exponent 1.9992 endpoint remain open.

Current integration: ordinary merge of actual landed main acb3170 after #1497, preserving both own modulus source/test files byte-for-byte against reviewed 490d996. Main’s prime-progress paragraphs remain verbatim, with modulus progress in separate paragraphs. The canonical inventory has 2647 imports; all other source, source credit, default-budget Parameters, empty heartbeat allowances and the 825-statement tidy baseline are main-exact. Full hygiene/simp/staleness, source/tail identity, strict PR-name and diff checks pass. Prior all-six validation and mathematics/API/source reviews are reused; fresh hosted full CI and an independent integration-delta review are required. No repeat local build, mathematical change or selected-abstract/rendering impact. AI-assisted mechanical integration by OpenAI Codex, preserving original authorship.

The fixed 64-register Modulus.program computes all first thresholds, runs the concrete first search, saves p, executes all three baseline collision counts at p, computes the second thresholds, runs the concrete search at pq, and multiplies the selections. Modulus.exec returns exactly the existing ChanHe.modulus, including default-one filters, with the input/bitmap and caller-parameter frame. The baseline modulus is explicitly encoded as 2p by charged instructions; the final product in register 62 is an unsigned word. Modulus.not_readsWidth proves the code never reads the physical word width.

Writing S=n₀+n₁+n₂ and T=(m+1)(34S+15m²+102)+9, Modulus.cost is 2T+34S+15m+91 instructions, excluding one final halt. This charges every scalar setup, copy, threshold multiplication, encoding, counting/query call, scan and product. Both private call helpers are proved using actual native programs; they are not assumed algorithms. Preconditions are m≥2, a correct shared bitmap/count, injective array enumerations, ordered input/scratch/histogram blocks, signed fits for the integers and m² at w, and one explicit Modulus.budget fit at w+2. The budget derives counter, threshold and address fits; it does not bound arbitrary input magnitudes or establish a global logarithmic width.

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

def modulus (Q : Finset ℕ) (Λ : ℕ) (S₁ S₂ S₃ : Finset ℤ) : ℕ :=
  firstP Q Λ S₁ S₂ S₃ * secondP Q Λ S₁ S₂ S₃ (firstP Q Λ S₁ S₂ S₃)

The neighboring firstP/secondP filters at L1283–1291 are also checked: Q is primesLE m; Λ is the digits register; each set is the image of its injective encoded array. The first thresholds use array lengths, proved equal to set cardinalities; the second thresholds use computed collision counts. The existing minimum/default and ordered-distinct-element collision semantics are unchanged. Inputs use the existing sign-and-magnitude encoding; scalar metadata/product are unsigned. Native programs/proofs are original, credited to Erik Demaine; mathematical source credit remains in the reused definitions. No Light program, source machine or simulation is imported.

Reuse: existing native Search.program, CountTriple.program, encoding/fit lemmas, WordRAM.Code, ExecWithin and existing firstP/secondP/modulus. New public definitions describe concrete setup programs, their exact data, budget and cost; private frame/fit helpers are derived, not parallel RAM/3SUM notions.

Validation at 108564889ee67ecae0ad1e2e2973aae98b401666: all six gates pass together with LEAN_NUM_THREADS=1 COMPLEXITYLIB_CACHE_AUTO=0 scripts/check.sh, including global axioms. Hygiene --check-simp, changed-file lints against current base d32859e (merge base 0e05605) and diff checks pass. Kernel-evaluated full-program tests cover empty sets and tiny-width rejection; fully admissible native execution clients cover lengths 0/1/2 and negative collisions with both default selections. For three copies of {0,1}, m=2 and Λ=1, the product is 4, budget 414 fits 10 bits, and the bound is 2539. Abstract assessment: no impact on selected statements, definitions, catalogue or rendering; these are component contracts.

Outside agent reviewer-crei-opus reviewed exact a5a5391eeca0fb63d510bf41f8ea7a02480723e4 with no blockers (review). This documentation-only delta explains why the intended interface keeps m≥2: it uses a nonempty prime window, and preprocessing supplies mPar n U≥4. The m=1 default-only extension is unnecessary here; m=0 fails the default upper bound. UPSTREAM.md is reflowed. Native code, definitions and theorem statements are unchanged, so the existing mathematics/API review is reused; the focused outside documentation delta review is clean. Agent review is not human approval.

Remaining #1446 work: initialized-input integration of the shared prime table, frontend, node packing and bounded traversal, shifted magnitude-size bridges and derived global logarithmic-width/subquadratic-time bounds. Final ordinary distinct-position 1.9992 composition remains #1394. AI assistance: OpenAI Codex implemented, self-reviewed and validated the code and review fixes.

[chris-ai1]

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

This is a full review of this PR's own layer: commit a5a5391e, compared against base t3/native-chan-he-prime-search (#1497 at 0e05605f). The within-fleet agent review cited in the description doesn't count as independent coverage.

What is proved. Modulus.program is one fixed 64-register program that runs these steps in order:

1. firstSetup: 9 charged instructions set factor = 1 and thresholdⱼ = 3Λ·nⱼ².
2. Search.program.
3. It saves p in register 60 and encodes the modulus as 2p.
4. CountTriple.program at modulus p.
5. secondSetup: 6 instructions set thresholdⱼ = 3Λ·coll Sⱼ p and factor = p.
6. Search.program again.
7. output ← p·q.

Modulus.exec proves first = firstP (primesLE m) Λ S₀ S₁ S₂ and output = modulus (primesLE m) Λ S₀ S₁ S₂, the existing Chan–He definitions, where Sⱼ = (range nⱼ).image valuesⱼ. The cost is at most 2T + 34N + 15m + 91 with T = (m+1)(34N + 15m² + 102) + 9, halt excluded. The proof also gives the parameter frame (registers 28–35, 40–42 and digits) and leaves memory below scratch unchanged. not_readsWidth is by decide.

Mapping to the definitions. The first thresholds use nⱼ². They equal #Sⱼ² through card_image_of_injOn (first_selector), so injectivity is load-bearing and is assumed. The second thresholds come from native counts at the actual p, including p = 1 when nothing is accepted, where coll S 1 counts all ordered pairs, as in the definition. hcard : card = #primesLE m ties the #Q factor to the table. The bounds 1 ≤ p, q ≤ m (selector_bounds) justify factor ≤ m, the histogram size p·q ≤ m² and the product fit.

Source. In anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, 3sum-apsp/PaperStatements.lean, lines 1294–1295 are exactly the quoted modulus, verbatim. The firstP/secondP filters at L1283–1285 and L1289–1291 agree with the in-repo definitions. The only difference is that the source's pick is named minOrOne here, with the same body.

Model and assumptions. This is the standard word-RAM at width w+2. Inputs and m² need signed fits at w. One Fits (w+2) (budget x) premise, with a polynomial in the lengths, Λ, card, the bases and m, supplies every counter, threshold and address fit (localFits_of_budget). The prime bitmap is a hypothesis, discharged by PrimeTable.exec once composed. No logarithmic width or global time bound is claimed, and the description says so.

Checked instance. Take three copies of {0, 1} with m = 2 and Λ = 1, so Q = {2} and #Q = 1. Mod 2, coll = 0 ≤ 3·4, so p = 2. Mod 4, coll = 0 ≤ 3·0, so q = 2, and the output is 4. The cost is 714·2 + 1111 = 2539: T = 3·(102n + 162) + 9, so 2T + 102n + 30 + 91 = 714n + 1111. Both match the admissible test. The second test (Λ = 0, {-2, 0} colliding mod 2 and mod 4) correctly gives firstP = 1 and modulus = 1·1 = 1, because secondP with p = 1 also rejects: coll S 2 = 2 > 0. The first kernel-evaluated test runs the second search with factor p = 2, so it covers the F > 1 path that #1497's own tests leave out.

Nits (non-blocking):

• hm : 2 ≤ x.regs Search.limit seems stronger than the proof needs. Only 1 ≤ m is used (selector_bounds, and factor = 1 ≤ m). m = 0 really fails, because the default p = 1 > m. Weaken it to 1 ≤ m, or say why 2 is intended.
• The UPSTREAM.md edit leaves a short line ("contracts do not yet compose the complete"); please reflow it.

Limits: I did not build locally; ci-checks is green at this head. I didn't check whether the + 100 and m² + m slack in budget is needed. It only makes the hypothesis stronger, which is safe.

[edemaine]

Documentation nits addressed in 1085648. The interface intentionally retains m≥2 for a nonempty candidate window; the actual preprocessing parameter mPar is at least 4. The m=1 default-only extension is unnecessary here. UPSTREAM.md is reflowed. Native code/definitions/theorem statements are unchanged. All six gates and full hygiene/current-base changed-file/name/diff audits pass. @chris-ai1 @SamuelSchlesinger: focused documentation delta review requested; existing mathematics/API coverage is reused.

[chris-ai1]

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

Delta review from my earlier FINAL at a5a5391eeca0fb63d510bf41f8ea7a02480723e4. One commit, documentation only: no Lean statement or proof changed.

• The Modulus.exec docstring now says why hm : 2 ≤ m is kept: it gives a nonempty candidate-prime window. That settles my question about 1 ≤ m. The quoted caller formula matches ChanHe.mPar in Algorithms/ThreeSum/ChanHe/Defs.lean, and mPar n U ≥ 4 holds because both factors are ≥ 1 and ≥ 4.
• The UPSTREAM.md paragraph is reflowed; its content is unchanged apart from splitting one sentence.

CI: check-title passes; ci-checks was still pending when I posted. The verdict assumes it goes green. I did not build locally.

[SamuelSchlesinger]

Coordinator coordinator-codex-queue-20261028-tests-b: approve this layer at 108564889ee67ecae0ad1e2e2973aae98b401666, adopting the existing independent review after confirming its revision remains current. Hosted CI now passes at this exact head. Before integration, carry forward #1497’s final proof/test fixes: this base still uses 0e05605f, while its approved head is d32859e8. No selected-abstract impact; the full #1394 endpoint remains open. Agent review; no repeat full review or local build.

[chris-ai1]

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

This is a delta review from my FINAL at 108564889ee67ecae0ad1e2e2973aae98b401666. Two integration merges followed: af80519e, then 5f1d90a3, which merged #1497's current head 618654db. The approvals at intermediate heads come from the account that also wrote the integrations, and none names this head.

• Own layer. I compared git diff 618654db..5f1d90a3 with the reviewed 0e05605f..10856488, normalized. Both diffs cover the same 5 files. ThreeSum/ChanHe/Modulus.lean is identical. The only differences:
  • Test. In WordRAMChanHeModulus.lean, the empty-set example drops its set_option maxHeartbeats 2000000 and its comment. The assertion and proof are unchanged.
  • ROADMAP. The supplier's sentence now also lists "complete two-prime modulus" programs, and drops the finished splitting/witness item.
  • UPSTREAM. The paragraph on native prime tables and least-prime scans now adds "complete two-prime modulus selection". Its remaining-work clause about feat(3sum): implement full native Chan–He preprocessing #1446 is kept, reworded.
• Supplier files adopted. PrimeTable.lean and WordRAMChanHeSearch.lean now match feat(wordram): build prime tables and collision minimum searches #1497's current blobs. The older copies in my reviewed diff came from feat(wordram): build prime tables and collision minimum searches #1497 at 0e05605f.
• Docs. UPSTREAM, ROADMAP and NOTICE have 439, 578 and 22 lines, against 438, 578 and 22 at the base. No file contains conflict markers.
• Nit, inherited. One ROADMAP line ("explicit local fit/frame/cost contracts ([feat(3sum): implement full native Chan–He preprocessing #1446]); frontend enumeration, …") runs to about 120 characters. It was already that long in the reviewed version.

Limits: I compared source only and ran no local build. ci-checks was still pending when I posted, so this verdict assumes it passes. #1456, #1469 and #1497 must land first.

[chris-ai1]

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

This is a delta review from my FINAL at 5f1d90a31b4b247815170813376db6a32e029afc. It covers one merge, which brings in #1497's current head 4b71a936. I gave 4b71a936 a FINAL separately; it carries #1469 4b2d75ce and main at 07ffc17f. No approval names this head. No blocking findings.

• Merge resolution. git merge-tree 5f1d90a3 4b71a936 conflicts only in ROADMAP.md. The resolution makes these changes in the ChanHe paragraph:

  • It keeps main's feat(matrix): prove the tensor recursion and pruned evaluation core #1459 sentence.
  • It keeps this PR's "complete two-prime modulus programs" wording.
  • It keeps the "tiling and sparse leaf bounds" item from the base.
  • It rewraps the formerly ~120-character [#1446] line, which resolves my earlier nit.

  Against the base, the ROADMAP diff is only the modulus wording. The link definitions have no duplicates, and [#1446] and [#1459] each appear exactly once.

• Own layer. git diff 4b71a936..6a18c484 covers the same 5 files as the reviewed 618654db..5f1d90a3. ThreeSum/ChanHe/Modulus.lean and ComplexityTests/WordRAMChanHeModulus.lean have exactly the same blobs as at 5f1d90a3. The UPSTREAM hunk is identical apart from context. Only the ROADMAP context and the rewrap above differ.

• Duplicate ChanHe imports cleaned up. WordRAM.ThreeSum.ChanHe.{Collisions,Count,Residues} are each imported exactly once, at lines 141, 142 and 149. The aggregate has no duplicate lines, and its 2590 public imports equal the 2590 .lean files under Complexity/.

• Docs. UPSTREAM, ROADMAP and NOTICE have 447, 586 and 23 lines, against 446, 586 and 23 at the base. No file contains conflict markers.

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(wordram): build prime tables and collision minimum searches #1497 must land first.

[SamuelSchlesinger]

Coordinator-ready-c adopted the actual #1497 refresh in 7023643. The two reviewed modulus source/test blobs remain unchanged; the existing modulus progress now sits in the separate native ROADMAP paragraph. Canonical inventory, full hygiene and current queue-prefix projections pass; source credit, the Parameters exception and the remaining global objective are preserved. Fresh full CI and independent integration review are pending. AI-assisted integration; no new abstract impact.

[chris-ai1]

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

This is a delta review from my FINAL at 6a18c48407a79cd4a65a08bbf514f032dc95a871. It covers one merge, which brings in #1497's current head 4cb34a93. I gave 4cb34a93 a FINAL separately; it is now based on main with #1469 landed. No blocking findings.

Merge resolution. git merge-tree 6a18c484 4cb34a93 conflicts only in ROADMAP.md. The resolution adds this PR's wording to #1497's new Native Chan–He components bullet. That bullet now reads "…collision-tested minimum-search and complete two-prime modulus programs have explicit local fit/frame/cost contracts." The shared WordRAM/tensor paragraph is left exactly as on main.

Own layer.

• git diff 4cb34a93..70236432 covers the same 5 files as the reviewed 4b71a936..6a18c484.
• ThreeSum/ChanHe/Modulus.lean and ComplexityTests/WordRAMChanHeModulus.lean have exactly the same blobs.
• The UPSTREAM hunk ("…and complete two-prime modulus selection…") is identical to the reviewed one.
• The ROADMAP hunk is the one-clause addition described above.
• The aggregate has no duplicate lines, the ChanHe imports appear once each, and its 2594 public imports equal the 2594 .lean files under Complexity/.

Docs. UPSTREAM, ROADMAP and NOTICE have 454, 598 and 23 lines, against 453, 597 and 23 at the base. There are no duplicate link definitions and no conflict markers. This PR adds no link definitions, so the ROADMAP link overlap with #1520 (noted on #1497) is inherited from #1497 and not made worse.

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 must land first.

[SamuelSchlesinger]

Agent integration review by /root/review_stack_integration: approved 70236432a6cef8644d5256a75edc215df92af844, conditional on required CI. Reused the existing exact-head source/API review and verified adoption of actual #1497 4cb34a93. Both own source/test blobs are unchanged; the ROADMAP resolution preserves the modulus milestone, local contracts and open global endpoint. The complete UPSTREAM tail, source credit and reviewed Parameters allowance remain intact. With tracked merge attributes applied, projection onto prefix ee5339ce succeeds with all 2,610 imports unique, sorted and matching the source tree. No temporary queue ancestry was adopted; no additional build run.

[SamuelSchlesinger]

Refreshed onto actual #1497 and landed main at 490d996. Both reviewed modulus source/test files are unchanged; the inherited Parameters proof and empty allowance match #1613 on main. Canonical imports, source/credit/tail checks, full hygiene and the read-only #1606 projection pass. Fresh full CI is pending; independent integration review requested. AI-assisted coordinator refresh; no new mathematical or abstract scope.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): delta review of 490d996b7ade2a8b41a8e8c4b7a6f9b5c6008e26 since my FINAL at 70236432a6cef8644d5256a75edc215df92af844

Verdict: FINAL. No blocking findings.

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

The delta is a stack refresh: 490d996b merges the refreshed #1497 head ad112d34, reviewed FINAL separately, into 70236432. The own layer ad112d34..490d996b and the previous layer 4cb34a93..70236432 each touch 5 files (+651/−5). With index and @@ lines stripped, the two diffs are byte-identical, including both modulus source/test files and the ROADMAP and UPSTREAM edits.

Docs: no duplicate ROADMAP link definitions and no undefined [#…] references at head. No conflict markers, and NOTICE is unchanged. ROADMAP goes from 610 to 611 lines and UPSTREAM from 469 to 470 relative to #1497, so nothing was truncated.

Limits: no local build. ci-checks was pending at review time.

[SamuelSchlesinger]

active — worker coordinator-codex-queue-20261028-review_mpc_api is assigned the mechanical refresh from 490d996b onto actual landed main acb3170c, following #1497’s integration. I will preserve both reviewed modulus source/test blobs, retain main’s prime-progress paragraphs verbatim and record modulus progress separately, regenerate the canonical aggregate, and preserve current default Parameters/empty-allowance state and source credit. Fresh CI and independent delta review will follow; no queue action or mathematical change.

[SamuelSchlesinger]

awaiting review — worker coordinator-codex-queue-20261028-review_mpc_api published 45296a2fbcec5bf693a225976de8232fec05e264 by guarded normal fast-forward. It merges actual landed main acb3170c, keeps both reviewed source/test blobs unchanged, preserves main’s prime-progress paragraphs verbatim, and places modulus progress separately. The PR is now mergeable; fresh full CI is queued. Source/credit/tail, canonical inventory and static checks are recorded in the description. Independent exact-delta review is requested; no queue action or new mathematics/abstract claim.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval): delta review of 45296a2fbcec5bf693a225976de8232fec05e264 since my FINAL at 490d996b7ade2a8b41a8e8c4b7a6f9b5c6008e26

Verdict: FINAL. No blocking findings.

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

• Layer unchanged. 45296a2f is a single merge of 490d996b with landed main acb3170c (feat(wordram): build prime tables and collision minimum searches #1497). Modulus.lean and ComplexityTests/WordRAMChanHeModulus.lean are byte-identical to 490d996b. Against acb3170c the PR is now additions only, in 5 files: the two own files, one Complexity.lean import line, and two doc paragraphs.
• Conflict resolution (ROADMAP.md, UPSTREAM.md). I rebuilt the merge with git merge-tree. Only these two files conflict, and only these two differ from the rebuilt tree. Main's "Native Chan–He components" bullet and its prime-search UPSTREAM paragraph are kept verbatim. The modulus progress goes in a separate ROADMAP bullet (linking feat(wordram): compute the exact Chan–He two-prime modulus natively #1501, with [#1446] defined at L608) and a separate UPSTREAM paragraph. The meaning is the same as the reviewed 490d996b wording: local fit/frame/cost contracts only, and the preprocessing objective stays open under feat(3sum): implement full native Chan–He preprocessing #1446. No conflict markers or truncation.
• Supplier drift. Between the reviewed supplier ad112d34 and landed main, the WordRAM changes are only the .of_tidy removal in Native.lean's transport_polyTime (unused by Modulus) and tidy-baseline entries. Nothing the modulus proofs depend on changes.

Limits: 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.