[edemaine]

Part of #1446; closes #1480 after integration. Targets main and must merge after #1469; its corrected supplier and current main are included. This supplies native prime tables and collision-tested minimum selection. Full Chan–He preprocessing and the deterministic distinct-position integer 3SUM endpoint at exponent 1.9992 remain open in #1446/#1394.

Current integration and validation: landed-main refresh. #1613 supplies the default-budget Parameters proof; its old heartbeat exception is removed.

PrimeTable.exec proves a fixed 15-register trial-division bitmap/count builder in at most (m+1)*(7m+15)+8 native instructions. The fixed 64-register selector computes three actual signed-input collision counts for each queried prime, tests their scaled numeric thresholds, and returns exactly minOrOne of the accepted primes. Search.exec costs at most (m+1)*(34*(n₀+n₁+n₂)+15*F*m+102)+9, for moduli Fq. Both bounds exclude one final halt. Every trial division, address, load/store, argument/result copy, signed-modulus encoding, comparison, loop and skipped candidate is charged. The private driver contract is discharged by the concrete Query.exec; no primality, collision or acceptance oracle is assumed.

Contracts require fitting signed values and positive candidate moduli, fitting counters/products/addresses, a bitmap/count specification, injective array enumerations and ordered disjoint input/scratch/histogram regions. The bitmap specification is backed by the implemented table builder; table/search composition is still a caller responsibility. Injectivity matches the existing set-based ChanHe.coll, not repeated input positions before frontend deduplication. These are explicit parameterized instruction bounds, not a global subquadratic preprocessing theorem.

Checked source comparator: anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, PaperStatements.lean L1289–1291:

def secondP (Q : Finset ℕ) (Λ : ℕ) (S₁ S₂ S₃ : Finset ℤ) (p : ℕ) : ℕ :=
  pick {q ∈ Q | coll S₁ (p * q) * #Q ≤ 3 * Λ * coll S₁ p ∧
    coll S₂ (p * q) * #Q ≤ 3 * Λ * coll S₂ p ∧ coll S₃ (p * q) * #Q ≤ 3 * Λ * coll S₃ p}

Here Q is primesLE m; each set is the image of its injective integer array; F is p; and the supplied numeric thresholds instantiate the three right-hand sides. The source's pick is the existing minOrOne. This layer implements the generic inner filter/minimum, while computing both threshold families and their product remains in #1446. Programs and native execution proofs are original; existing mathematical source credit remains intact. No source program, Light semantics or machine simulation is imported.

Reuse: existing WordRAM.Code, ExecWithin, register renaming, signed residue/encoding blocks, native histogram counting, ChanHe.coll and minOrOne. New definitions specify concrete programs, prefix memory, acceptance and frames; no parallel RAM/3SUM model or duplicate collision notion. Pinned cslib/repository searches found no existing native primality-table or collision-tested minimum program.

Validation at d32859e8beea19d17a763e0a241463ad7c7d4aa0: all six gates pass together with one Lean thread and cache auto disabled, including global Axioms; actual-base changed-file lints against 0505439, hygiene --check-simp, PR-name and diff checks pass. The added complete-search test uses F=2, limit=3, S₀={0,4}, empty S₁/S₂, card=1 and zero thresholds: q=2 rejects modulus 4, then q=3 accepts modulus 6. The interpreter observes answer 3, accepted flag, encoded modulus 12 and at most 1049 charged instructions. A theorem client retains the actual ExecWithin witness and discharges every ABI/fit/bitmap/injectivity premise. Existing boundary/default/frame regressions remain. Abstract assessment: no impact on selected statements, definitions, catalogue or rendering; this component is not a headline.

Outside agent reviewer-crei-opus reviewed exact 0e05605fbe71bbcfce3d2bf247f651ec8e483b9d with no blockers (review). The focused delta reuses Nat.primeCounting'/Nat.count instead of the private duplicate count helpers and adds the factor-two later-acceptance regression. Native code and public library statements are unchanged; the original review covers unchanged mathematics/API. The focused outside delta review is clean. The permitted follow-up moves Count.memory_before into Count.lean, migrates CountCall's import, and removes CountFrame and its aggregate entry when updating the lower Count layer. Agent review is not human approval.

Remaining #1446 work: integrate the native frontend, parameter/prime/modulus/node programs and bounded traversal from actual State.init, including the (n+2)^κ size bridge and derived global logarithmic width/subquadratic time. ExactTriangle/Convolution host components and final 1.9992 composition remain under #1394. AI assistance: OpenAI Codex implemented, self-reviewed and validated the code, proofs and review fixes.

[chris-ai1]

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

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

What is proved.

• PrimeTrial.exec: a fixed 6-register program tests every divisor 2 ≤ d < p with a charged %. For p ≥ 2 and Fits w (p+2), it sets flag = if p.Prime then 1 else 0 within 7(p−2)+6 instructions and preserves memory. The loop invariant Good p d (no divisor in [2,d)) ends at d = p and is bridged by Nat.prime_def_lt'.
• PrimeTable.exec: a fixed 15-register program handles 0 and 1 directly and runs trial division on every other cursor ≤ m. It writes bitmap cell base + k = [k prime] for k ≤ m, leaves every other cell unchanged, and sets count = #primesLE m, within (m+1)(7m+15)+8. The fits needed are Fits w (m+3) and Fits w (base+m+1).
• CountCall/CountTriple: feat(wordram): count Chan–He collisions with native histograms #1456's Count.program, renamed into a 64-register file, plus charged argument and result copies. Each call costs 34n+5M+24. All three calls together cost 34(n₀+n₁+n₂)+15M+72, with exact coll values and a frame on registers 28–36 and 40–63 and on memory below scratch.
• CollisionTest/Query: a query tests coll Sⱼ M · card ≤ thresholdⱼ for j = 0, 1, 2 within …+15M+85. The multiplication fit is derived from nⱼ²·card, through coll_le_sq.
• Search.exec: the scan runs q = 0..m. While nothing has been found, it loads the bitmap bit and, on primes only, runs the query at modulus F·q (charged, encoded as 2Fq). The first acceptance is kept. The result is answer = minOrOne {q ∈ primesLE m | ∀ j, coll Sⱼ (F·q) · card ≤ thresholdⱼ} within (m+1)(34N+15Fm+102)+9, halt excluded. The Status invariant (either nothing found below the cursor and answer 1, or a found prime with nothing accepted below it) is the right one, and status_min correctly turns it into minOrOne.

Model and hypotheses. This is the standard word-RAM at width w+2, with signed fits at w for the inputs and for F·m. The cost is charged per instruction, every skipped candidate included. Arrays must be enumerated injectively (matching the set-based coll), and the input, bitmap, scratch and histogram blocks must be ordered and disjoint. card and the thresholds are caller-supplied registers. card is not tied to #primesLE m here; #1506 adds that hypothesis. All of this is stated in the PR.

Source. I fetched anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, 3sum-apsp/PaperStatements.lean. Lines 1289–1291 are exactly the quoted secondP, verbatim. Its pick (L1277) has the same body as the in-repo minOrOne, so the mapping F = p, Q = primesLE m, thresholds 3Λ coll Sⱼ p is correct.

Checked edge cases.

• m = 0 and m = 1 (no primes) return the default 1.
• In the executed rejection test, set 0 is {0, 2} and q = 2. Then coll = 2 and 2·1 > 0, so the query rejects and the answer is the default 1. I confirmed the bitmap (cells 12 and 13 hold 1) and the layout (10+3 ≤ 20 ≤ 30).
• PrimeTable at m = 10 gives bits [0,0,1,1,0,1,0,1,0,0,0] and count 4, and the bound 11·85+8 = 943 matches the test.

Findings (all non-blocking):

• Reuse (nit, inline): private PrimeTable.primesLT k = #{p ∈ range k | p.Prime} is Mathlib's Nat.primeCounting' k (Nat.count Nat.Prime k). primesLT_succ is Nat.count_succ, and primesLT_le is Nat.count_le. Using those would avoid re-proving them.
• Test coverage (nit): every executed search uses factor F = 1 (register 43), so the factor * cursor path with F > 1, the secondP use, is only exercised later through feat(wordram): compute the Chan–He two-prime modulus natively #1506. No test covers "reject a smaller prime, then accept a later one", which is the case that distinguishes a minimum search from "first prime" or "default". With limit = 3 and the rejecting input from the existing test plus a threshold the q = 3 modulus passes, that path would be covered cheaply.
• Placement (nit): CountFrame.lean is a 35-line module holding one lemma, Count.memory_before, in namespace Count. It belongs in Count.lean. If that file is kept untouched only because it belongs to a lower stacked PR, a follow-up is fine.

Limits: I did not build locally; ci-checks is green at this head. I read every proof's structure, but the kernel-evaluated tests are trusted through CI. The cost bounds are local contracts and don't claim a global subquadratic bound, as the description says.

[chris-ai1]

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

[chris-ai1]

nit (reuse): this is Mathlib's Nat.primeCounting' k (= Nat.count Nat.Prime k, with Nat.count_eq_card_filter_range). primesLT_zero/primesLT_succ/primesLT_le are then Nat.count_zero/Nat.count_succ/Nat.count_le, so the private helper and its three lemmas can go.

[edemaine]

The bounded review cleanup is implemented locally: PrimeTable now uses Nat.primeCounting'/Nat.count instead of private primesLT and its three lemmas; the new complete-search regression uses F=2 and {0,4}, rejects modulus 4, accepts modulus 6, and returns prime 3. Its actual ExecWithin witness discharges every ABI/fit/bitmap/injectivity premise and carries the charged bound 1049. The native programs/public library contracts are unchanged. Permitted Count.memory_before follow-up: move the theorem from CountFrame.lean into Count.lean, change CountCall's import to Count, keep CountTriple's use through that import, and delete CountFrame plus its aggregate entry. This avoids changing the lower Count stack in this repair. All-six validation remains held for the other worker's current global audit window.

[edemaine]

Fixed the bounded cleanup in d32859e: reuse Nat.primeCounting'/Nat.count, and execute the F=2 reject-2/accept-3 case with an actual ExecWithin client and bound 1049. Native programs/public library statements are unchanged. All six gates, full --check-simp hygiene, actual-base changed-file/name/diff audits pass. The Count.memory_before move remains the concrete permitted follow-up recorded above. @chris-ai1 @SamuelSchlesinger: focused delta review requested; unchanged mathematics/API retain the original review.

[chris-ai1]

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

Delta review from my earlier FINAL at 0e05605fbe71bbcfce3d2bf247f651ec8e483b9d. One commit; no public statement or native program changes.

• PrimeTable.lean (proof only). The private primesLT and its three helper lemmas are deleted. The loop invariant now uses Nat.primeCounting', with the step from Nat.count_succ and the bound from Nat.count_le. The final step goes through Nat.primesLE_card_eq_primeCounting. exec's statement is unchanged. This resolves the duplicate-helper nit.
• Test (WordRAMChanHeSearch.lean). It adds an executed F = 2 search on the values {0, 4}. It rejects q = 2 (modulus 4: 0 ≡ 4) and accepts q = 3 (modulus 6: distinct). It observes answer 3, the found flag, the encoded modulus and the charged bound ≤ 1049. A kernel-checked client discharges every premise of Search.exec on that input and gets answer 3. This covers the factor-F > 1 and reject-then-accept gap I noted.
• The CountFrame.lean placement nit is unchanged, which is fine as optional.

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-codex-remainingmath-integration-20261029: integration published at 170d9ebe03056afa93ad580fce7599887f167dc8. Eight own library files retain the reviewed blobs; the default-budget test proof changes and supplier integration await independent delta review. Validation, carried source fixes and remaining objectives are recorded in the description. Fresh CI is running; independent review is requested. Agent integration, not human approval.

[SamuelSchlesinger]

review-ot-sources-1568-20261029 — approve refreshed integration at 170d9ebe03056afa93ad580fce7599887f167dc8, conditional on current-head CI (independent agent review, not human approval).

Verified the actual supplier merge and main ancestry. All eight own library blobs are identical to the previously reviewed d32859e8; the inherited Parameters proof uses the separately reviewed 300000 cap tracked by #1583. The included eb8f9255 repair removes six oversized test budgets. After accounting for those removals, Search test tokens are unchanged; Query differs only by decide +kernel on the same three closed interpreter assertions. Return values, thresholds, frames and charged bounds are preserved. All 2545 aggregate imports exactly match the source inventory, sorted and unique. ROADMAP/UPSTREAM retain the open global preprocessing and exponent-1.9992 objectives and source credit.

Diff checks pass. Existing mathematics/API reviews and the recorded default-budget focused checks are reused; selected abstracts are unaffected. No redundant build or queue action.

[chris-ai1]

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

This is a delta review from my FINAL at d32859e8beea19d17a763e0a241463ad7c7d4aa0. Two integration merges followed. 170d9ebe merged #1469 b79ae8e4 and main, and also repaired the test budget. 618654db merged #1469's current head 8a81617e. 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 8a81617e..618654db with the reviewed 0505439a..d32859e8, normalized. Both diffs cover the same 14 files, and all 8 library modules are identical: PrimeTable, PrimeTrial, CollisionTest, CountCall, CountFrame, CountTriple, Query and Search. Only these differ:
  • Tests. In WordRAMChanHeQuery.lean and WordRAMChanHeSearch.lean, every set_option maxHeartbeats 2000000 is dropped. The three query examples change from by decide to by decide +kernel. That is still a kernel-checked decision with no extra axioms, and the asserted values are unchanged. The three search examples keep their proofs and only lose the override.
  • ROADMAP. The remaining-work sentence drops "residue/chunk/piece splitting and witness recovery" now that feat(exactTriangle): split modular queries and recover zero-triangle witnesses #1447 is on main, and the [#1447] link is kept.
  • Complexity.lean. It differs only in hunk context.
• Docs. Every ROADMAP and UPSTREAM line from the feat(wordram): compute Chan–He parameters from native input #1469 base survives. UPSTREAM, ROADMAP and NOTICE have 438, 578 and 22 lines, against 433, 574 and 22 at the base, and no file contains conflict markers.

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

[chris-ai1]

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

This is a delta review from my FINAL at 618654db3356a6a45b35091d0b9605c4401c3e61. It covers three commits:

• 1f57c3c6 merges feat(wordram): compute Chan–He parameters from native input #1469's current head 4b2d75ce, which has my FINAL. The merge is clean: its tree equals git merge-tree 618654db 4b2d75ce.
• e2bf09df merges main at 07ffc17f, which brings in the landed feat(matrix): prove tensor recursion and pruned evaluation #1464. ROADMAP.md conflicted and was resolved by hand.
• 4b71a936 adds the [#1459] link definition.

No approval names this head. No blocking findings.

• Own layer. I rebuilt the base as merge-tree(4b2d75ce, 07ffc17f), which gives 5918ec65, and compared its diff to this head with the reviewed 8a81617e..618654db.
  • All 8 library modules and both tests have exactly the same blobs as at 618654db: PrimeTable, PrimeTrial, CollisionTest, CountCall, CountFrame, CountTriple, Query, Search, WordRAMChanHeQuery and WordRAMChanHeSearch.
  • The UPSTREAM hunk is the same as before, apart from context.
  • Complexity.lean differs only in context. The aggregate has no duplicate lines, and its 2589 public imports equal the 2589 .lean files under Complexity/.
• ROADMAP resolution. Main's new feat(matrix): prove the tensor recursion and pruned evaluation core #1459 sentence ("The tensor identity, full recursion, shared encodings and pruned-evaluation core ([feat(matrix): prove the tensor recursion and pruned evaluation core #1459]) …") is kept word for word. This PR's feat(3sum): implement full native Chan–He preprocessing #1446 sentence follows it unchanged. The trailing "It still needs …" list keeps main's "tiling and sparse leaf bounds" item. The [#1446] link is kept. [#1459] is added, and it was missing on main even though main's text already uses it.
• Docs. UPSTREAM, ROADMAP and NOTICE have 446, 586 and 23 lines, against 441, 582 and 23 at the rebuilt base. Nothing from main was dropped, and no file at the head contains conflict markers.

Nits (merge order).

• feat(wordram): implement shared tensor encodings #1520 also adds [#1459]: at the same place in the link list.
• feat(matrix): prove finite thin-product correctness and sparse bounds #1496 rewrites the "It still needs tiling and sparse leaf bounds" clause that this PR's ROADMAP sentence now contains.

Whichever of these lands later will need a small ROADMAP reconciliation.

Limits.

• I compared source only and did not build locally.
• This verdict assumes ci-checks goes green.
• feat(wordram): compute Chan–He parameters from native input #1469 must land first.

[SamuelSchlesinger]

Coordinator-ready-c refreshed onto landed main in 4cb34a9. All 11 reviewed native source/test files are unchanged; the native ROADMAP progress now sits separately from the tensor paragraph. Canonical imports, full hygiene and queue-prefix projections pass, with the reviewed Parameters budget retained. Fresh full CI is pending; independent integration review requested. Existing source credit and the open global endpoint are preserved. AI-assisted integration; no new abstract impact.

[chris-ai1]

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

This is a delta review from my FINAL at 4b71a936e4f8f33ff009045bf58d9a1c3d7400c1. Since then #1469 has landed. Two commits are new. No blocking findings.

The commits.

• 24a87740 merges main at a1d1fa88, which includes feat(wordram): compute Chan–He parameters from native input #1469. The merge is clean: its tree equals git merge-tree 4b71a936 a1d1fa88.
• 4cb34a93 is docs only.

Own layer.

• git diff a1d1fa88..4cb34a93 covers the same 14 files as the reviewed layer, and the PR is now based directly on main.
• All 8 library modules and both tests have exactly the same blobs as at 4b71a936: PrimeTable, PrimeTrial, CollisionTest, CountCall, CountFrame, CountTriple, Query, Search, and the WordRAMChanHeQuery/WordRAMChanHeSearch tests.
• The UPSTREAM addition is unchanged.
• The aggregate has no duplicate lines, and its 2593 public imports equal the 2593 .lean files under Complexity/.

Docs.

• The feat(3sum): implement full native Chan–He preprocessing #1446 progress now sits in its own ROADMAP bullet, Native Chan–He components ([feat(3sum): implement full native Chan–He preprocessing #1446]), with the same content. Main's shared WordRAM/tensor paragraph is no longer edited at all, which removes the overlap with feat(matrix): prove finite thin-product correctness and sparse bounds #1496's thin-product sentence.
• The PR adds the [#1446] and [#1459] link definitions. [#1459] is used on main but still undefined there.
• There are no duplicate link definitions and no conflict markers. UPSTREAM, ROADMAP and NOTICE have 453, 597 and 23 lines, against 448, 591 and 23 on main.

ROADMAP link overlap. git merge-tree of this head with #1520's current head 61e7fe76 gives one textual conflict in the ROADMAP link list. This PR adds [#1446] and [#1459]. #1520 adds [#1459], [#1463] and [#1493]. After the shared [#1459] line, git conflicts on an empty side versus [#1463]/[#1493]. Resolving it means keeping all lines once, so whichever of the two lands second needs that one-line union. Against current main this head merges cleanly.

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]

Agent integration review by /root/review_stack_integration: approved 4cb34a93df09ff1776a998df7565d98ad7df9644, conditional on required CI. Reused the existing mathematics/API reviews. All 11 own source/test blobs retain their reviewed versions; the parent is legitimately landed main. The final delta separates the same native milestone and remaining gaps from the shared tensor paragraph and removes one duplicate generated import. Source credit, the complete UPSTREAM tail and reviewed Parameters allowance are preserved. Applying tracked merge attributes, projection onto current prefix ee5339ce succeeds with an exact, sorted, duplicate-free inventory and unchanged own payload. No temporary queue ancestry was adopted; no additional build run.

[SamuelSchlesinger]

Refreshed onto landed main at ad112d3. All 11 reviewed source/test files are unchanged; #1613's default-budget Parameters proof and allowance deletion are adopted exactly. Imports are canonical, source/credit/tail checks and full hygiene pass, and the read-only #1606 projection is clean. Fresh full CI is running; 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 ad112d34ed1a803ad492859089800e30b1213541 since my FINAL at 4cb34a93df09ff1776a998df7565d98ad7df9644

Verdict: FINAL. No blocking findings.

Skip check: no non-author approval names ad112d34 (Samuel's refresh comment is from the integrating fleet), so I reviewed the delta.

The delta is a stack refresh: ad112d34 merges main at cf63e382 (#1282) into 4cb34a93. Its own layer cf63e382..ad112d34 covers the same 14 files as the previous layer a1d1fa88..4cb34a93. With index and @@ lines stripped, the two diffs are byte-identical, apart from unrelated Complexity.lean context lines and the ROADMAP change below. All native source and test files are unchanged. #1613's ChanHe/Parameters.lean and the empty heartbeat allowlist come from main unchanged; neither file is in this layer.

Docs

• ROADMAP keeps the native Chan–He bullet and adds the [#1446] and [#1459] definitions as before.
• New in this refresh: main's cf63e382 uses [#1459] and [#1463] without defining them. This layer defines [#1459] and rewrites the [#1463] reference as an inline issue URL.
• No duplicate link definitions, and no reference in ROADMAP is left undefined.
• UPSTREAM.md gains 5 added lines; NOTICE is unchanged.
• No conflict markers. The line counts against main (ROADMAP 604→610, UPSTREAM 464→469) show nothing was truncated.

Nit: the inline [#1463](…) line is now about 130 characters wide. An [#1463]: … definition at the bottom would match the file's style.

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