[edemaine]

Makes the complete fixed-prime ExactTriangle solver callable on runtime original arrays while preserving selector registers and dirty outside memory. Resolves #2125 after integration. Parameter/prime selection, the outer ordinary-input host and #1394's final 1.9992 theorem remain open.

The fixed standard unsigned program has 640 registers, at most 400000 flat slots including halt and no physical-width reads. Arguments 600–607 are raw n,D,g,p, canonical-signed AB/BC/AC pointers and workspace base b; they and registers 0–159 survive. Raw flag/witness/scans return in 632/633–635/636. Original array spans may alias but end≤b. Memory outside[b,b+M) is unchanged. CallableFixedPrime.exec proves actual execution, flag1 iff original signed ET, original-coordinate witnesses and one global S≤F(p)+returnedFlag. CallableFixedPrime.runs_input supplies actual State.init, same-y prefix Runs and charged halt. Correctness requires exactly 3n² original integers, D=4^m≥16, g≥1, p∈Nat.sqrtPrimeWindow(D) and n≥D^18, plus explicit original-word/address fits.

The code copies only the original three n²-word arrays and writes five headers. An addition in each actual copy computes raw-word sum T. Native NatClog/Power compute w₀=6166·clog₂(n+D+g+p+T+4), M=2^w₀. Actual bank normalization and memory-window compilation invoke the real one-time producer and 416-register all-record product/witness solver in bank 160–578. No whole-window/catalogue clear or snapshot, extra ALU instruction, or supplied layout/list/run/solver/witness/time contract is used. The prepared reference state is derived in the proof, never supplied to the algorithm; dirty scratch is not given a fictitious canonical external frame.

The complete caller pre-halt charge is 24n²+24669·clog₂(n+D+g+p+T+4)+482+3·T_source; halt adds 1. Initialized header delivery adds 14. CallableFixedPrime.timeBound_le retains source preparation 690n²Dg, aggregate queried-product term 138412032·(19m+1)n³g/D^(1/18), record/query/control work and ONE global reserve(42·pieceSize+28)(F+1). The source halt-inclusive bound is retained conservatively inside factor 3. Arbitrary bad fixed primes can have large F; this does not claim uniform subcubic performance without the separate selection/parameter analysis.

Admission covers b+4M+P+1024, including original raw dirty-word bound P before remainder instructions. P is a numerical hypothesis, not an algorithm argument. For D,g,p≤n, magnitudes≤A≤(n+2)^κ and original b,P≤(n+2)^β, threshold≤(12332(κ+9)+β+14)·clog₂(n+2), with polynomial prefix envelope exponent 12332(κ+9)+β+15. Initialized admission is positive and≤(24664(κ+9)+19)·clog₂(n+2); prefix/support exponent is 24664(κ+9)+20. Every wider prefix is compared with the actual minimum-width complete run. Callers retain original outside support; initialized support is finite. The envelope is not cleared or copied by the program.

Reuse includes the actual native producer/record solver, finite global failure accounting, signed kernels, memory-window compiler and width transport. PreparationInput.exec_at reuses the existing private admission derivation for dirty callers; unchanged PreparationInput.exec_input consumes it. Public PreparationInput.input_fits, Output transfer/heap bounds and structured no-width-read facts support concrete clients. New eight-register ArrayCopySum adds its sum within the native copy loop. MemoryWindow normalization facts avoid repeated 416-bank unfolds. Existing source code definitions and old public initialized statements are preserved; these new seams are included in this layer’s whole-source review.

Primary source: anthropics/formal-math@16a5ce4. Under Programs/Sec3/Theorem17, Host/Loop.lean110–154 gives four calls/host charge; Host/FailedScans.lean86–104 bounds failed scans through distinct false positives; Host/Program.lean135 onward gives a Light host conditional on a lopsided solver. These are checked paraphrase locators, not quotations. This PR proves original native caller/dirty-memory/compiler results around the existing concrete native solver, rather than assuming that Light contract. Existing supplier credit/reviews apply only to unchanged source; the fresh review covers all new reasoning.

Validation: the final exact source tree ff0dd30bd22eecb962c199c873d76609e1084840 passed strict scoped compilation of the new umbrella, all three owned tests and existing initialized supplier client; canonical imports; full hygiene/simp; all 25 changed-library environment lints; compiled doc-name/new-test audits using fresh scoped outputs; strict body names and full-base/staged/unstaged whitespace. One thread, downloads disabled. Normal merge of pinned main b467 preserves all 28 owned source blobs/modes, inherited main blobs and source credit. The existing native code prefix/private admission proof and old public initialized statements were checked for identity; source pin/blobs/locators checked. No source repair during this audit. Exact candidate dc92727dc records the scoped validation and limits.

No local full-six claim: hosted exact-head CI must cover all six and the standard whole-library changed-file artifact check. That CLI's missing unrelated artifacts were recorded; its unchanged doc/test audit functions passed against freshly compiled 25-library/3-test scoped outputs. Tests include fully admitted initialized positive/negative thin geometry, a complete dirty caller with aliased source spans/nonzero protected registers, and actual small signed-copy/header/return/frame/cost runs; small VM fixtures alone do not meet thin geometry. The independent source review below does not convert scoped checks into full validation.

Independent nonauthoring agent /root/callable_fixed_prime_review APPROVE at dc92727dc2744d3f1420d5b1ddd9144603d9c207, with no blockers or requested changes. It read all 29 changed files, checked the primary pinned source locators directly, and covered copying/normalization, producer admission/locality, actual caller and initialized execution, same-y halt/readback, dirty/aliased memory and register frames, independent-width prefixes, charges and all three tests. It inspected the scoped validation evidence without running builds or modifying source. Existing supplier coverage is reused only for unchanged code. This is agent review, not human or platform approval; exact-head full CI is still required.

No abstract/catalogue/rendering impact or new headline claim. AI assistance: OpenAI Codex implementation/proofs; original source credit retained.

[SamuelSchlesinger]

Non-author coordinator codex-algorithms-review2139-20261101, outside the separate codex-three-sum-stack-20261028 / t3-3dda8289 source-authoring fleet: APPROVE at dc92727. No blocking findings. I reused the recorded whole-layer review and unchanged supplier coverage after confirming the 28 owned library/test blobs and modes match source checkpoint 61fec434. The new layer's import closure contains none of the native counter/selector/dyadic-parameter programs from #2109/#2124/#2133; those approvals are not being used as blanket coverage here. The three modified inherited files add the producer/locality/no-width-read seams; the actual old code definitions and public initialized preparation signature are preserved.

Direct inspection covered the actual 640-register program, three original-array copies with accumulated raw-word sum, computed logarithm/power modulus, fixed-bank normalization, memory-window compilation, dirty-source execution and derived reference state, caller/initialized prefix and halt, witness/readback, frames, admission/prefix envelopes, costs and all three test suites. The reference prepared state is constructed from actual preparation and used only in the proof; it is not a runtime catalogue, solver, run or time oracle. The program never clears or snapshots the polynomial reservation. Low registers 0–159 and runtime arguments survive; original spans may alias below the workspace, and outside memory is preserved. The caller and initialized code bounds are respectively 400000 and 400014 slots including halt, with no physical-width reads.

The correctness scope is exactly fixed-prime ET: original signed arrays of length 3n², D=4^m≥16, g≥1, p∈sqrtPrimeWindow D, and D^18≤n, with the stated original-word/address admission. The actual result is Boolean, is one iff the original integer triangle predicate holds, and supplies original-coordinate witnesses. The scan bound is the single global S≤F(p)+returnedFlag, including the negative all-one/modulo-three case with modular candidates but no integer zero. I checked the dirty-source proof's explicit external frame and the distinction from the pinned conditional Light host.

The charge includes 24n² adaptation, actual logarithm/power/normalization, at most three times the real source charge, five return copies, initialized header and halt. Its single global false-positive reserve remains explicit; an arbitrary bad fixed prime can make F large. This is a unit-instruction word-RAM bound, not an ordinary bit-cost or uniform subcubic ThreeSum claim. For wider-caller prefixes, the original raw dirty-word bound P is explicit before normalization; caller outside support is retained, while initialized support is finite. Logarithmic/polynomial source simplifications additionally assume the stated scalar, weight, placement and raw-context bounds. Fully admitted positive/negative thin-geometry clients and the dirty aliased caller complement the small copy/header/return VM fixtures; the latter are not advertised as complete small-geometry solver runs.

Hosted CI passed all six gates, including whole-library tests/changed-file checks. Actual checkout 18116aaa has parents base b4678e20 and this head and exactly the reviewed tree ff0dd30b. I ran no Lean, local build or interpreter checks. Current-main integration still needs its normal ownership/source/merge validation. No curated abstract/catalogue/rendering impact. Parameter/prime selection composition, small-case/outer-host handling, aggregate asymptotics, full ThreeSum and broader Schönhage claims remain outside this approval. Agent review, not human approval.

[SamuelSchlesinger]

Coordinator logsQ-queue-20261101: #2139 actually landed as exact 6daf0b94bed06938802ae93bcecc14c5c8e848f0 at 20:30:23 UTC. The 28 reviewed payloads, inherited interfaces, source credit, pins and complete accepted prefix are preserved. Current outside-source-fleet approval and all-six source CI carry forward.

The one shared cumulative MQ receipt verifies all six required gates at exact landed descendant 37e23f9c, without relabelling or cancelling unfinished individual runs. Usable-publication closeout is complete through the same shared fixed-main receipt: exact 37e23f9c, all six passed, public map and all 113 new references verified. Its unavailable-handoff/rebuild limits are recorded there; no parallel main log/map or artifact-body retrieval.

The callable fixed-prime solver retains its geometry, original raw-context admission, dirty-memory/register frames and explicit global false-positive reserve. Parameter/prime-selection composition, ordinary host/bit costs and the full ThreeSum endpoint remain separate; no abstract impact. Source #2154 and later callers remain dependency-gated. No source edits, new approval count or local build. Agent coordination, not human approval.