Repository navigation
feat(ExactTriangle): solve every native catalogue record at a fixed prime #1662
Description
Active bounded implementation under #1394, following per-record witness #1639 / #1661 at d4b0493. Owner: worker/session codex-three-sum-continuation-t3-3dda8289, personally on ordinary child work/three-sum-native-fixed-prime-et-20261029 in the existing checkout. Fresh open issue/PR searches found only prerequisite per-record and finite-mathematical tasks, no competing all-record implementation. Root explicitly revises the earlier record-loop boundary and delegates this fixed-prime traversal; root retains global D/g/m and prime selection plus the ordinary outer host/final 3SUM composition. Published #1661 and ancestor remotes remain frozen.
Implement one fixed native program from actual original input: run the real producer ONCE, read its actual occupied count/record pointers, advance actual ordinals, invoke the complete concrete 400-register product/witness program with its unchanged 320/163-bank ABI, reuse scratch, and stop after the first verified original witness. Native reads/control/copies/calls/return/loop/halt must all be charged. No precomputed instance list, layout, run/time, sparse-execution or solver/witness certificate is an algorithm input. Preserve original signed weights and the existing single charged raw01-to-signed conversion.
Acceptance:
- Positive AND negative original-input ExactTriangle correctness across ALL records, actual State.init, same-state prefix Runs and charged halt, original-coordinate witness on success, fixed finite code/register count, and an actual producer-output/count/readback bridge to existing finite instanceIndices. Keep D=4^m>=16, L=19m, n>=D^18 and every original prime/scalar/weight assumption explicit.
- Sound scratch reuse and frames. A callee dirties memory above the producer heap: use actual Output definitions/locality and protected catalogue readback, rather than claiming its original full frame survives. Add only a small useful public locality/caller seam on this child if required, with real clients; reuse existing public fit/width APIs, without copying private fit proofs. No ancestor remote edits.
- GLOBAL scan accounting from actual ordinal/rank nonrepetition: inject executed failed (record,query) occurrences into existing global failedScans/distinct modular false positives, and prove total successful-return flags <=1. Derive total scans <= falsePositiveCount + final actual flag; do not sum a per-record F allowance once for each record. Preserve occurrence/list semantics.
- Charge preparation exactly once and all actual product/local setup/query/scan/controller costs. Derive aggregate queried-product and instance/query-count bounds using existing finite APIs, including card(instanceIndices)<=4ng where admitted. Keep preparation 690n^2D*g separate, retain explicit fixed-prime F(p) dependence and clearly record any remaining quantitative gap; no aggregate-saving assumption or endpoint promotion.
- Derive physical dirty-load/address fits, positive original-input logarithmic admission and polynomial all-prefix words/support independently of every larger admitted W. Provide meaningful native controller/scratch/short-circuit tests, both ET decisions and fully admitted producer-to-all-record clients; do not weaken geometry for small VM examples.
Pinned source: anthropics/formal-math@16a5ce4, 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Host/{Loop,InstanceData,InstanceFacts,FailedScans,InstanceCount}.lean and existing finite ExactTriangle.Witnesses/Splitting. Rebuild directly in native WordRAM; no Light simulation or assumed source procedure. Material differences: the existing native producer prepares its entire chunk-major catalogue/matrices once; source Host.Loop uses piece-major visits and writes each instance in its round. This native controller may stop later product calls after success. Correctness/accounting are derived for the actual native order, not asserted to be the source trace.
This milestone decides ET for admitted fixed parameters/prime; it does not choose those parameters or the prime, handle the unrestricted small geometry through a new global host, prove the final aggregate subcubic source exponent, or complete ordinary distinct-position 3SUM 1.9992. #1394 remains open. Source credit and abstract no-impact assessment remain required.
Source/MCP only now: ROOT retains the sole import/global/static slot. No import generation, global/static audits, new PR/publication or review agent before explicit coordination. Checkpoint source and request a final validation slot when complete; final six/static and fresh exact-head independent review precede publication. No new agents/providers, rebase/force, child watch/approval/merge. Prioritize any requested #1661 repair.
Activity
edemaine commentedon Oct 29, 2026
Source checkpoint 9ed49005c implements the actual one-time producer and all-record fixed-prime traversal, with original positive/negative ET correctness, dirty-workspace frames, same-state initialized prefix/halt, global
S≤F(p)+returnedFlag, logarithmic admission and width-independent polynomial prefix/support bounds. The charged aggregate theorem keeps preparation, products, query/root/control work and the single global scan reserve separate. Original geometry and prime hypotheses remain explicit; #1394 is open.Lean MCP is clean on the final umbrella and all three new test modules, including fully admitted positive and negative initialized clients and concrete controller/dirty-frame regressions. Final canonical imports, all six gates, static/source audits and fresh whole-layer independent review remain pending. Root retains the sole audit slot; this is a source checkpoint, with validation/limits in the commit description. No PR opened. The exact supplier doc fix will enter only through the later coordinated compatibility merge; no ancestor or toolchain changes were made.
chore(ExactTriangle): merge pinned rc2 prerequisites for validation
chore(ExactTriangle): validate fixed-prime native solver on supported…
edemaine commentedon Oct 30, 2026
Ready for root-arranged review at 52b94d0ed. All six gates pass on the exact supported-rc2 tree, including all three new suites, Smoke and global Axioms. Final hygiene/simp, pinned-base library/test/name/whitespace audits and source/quote/supplier identities pass. Four compiler threads were used after resource checks, with downloads and automatic cache restoration disabled during gates. The commit description records validation, premises, source mapping and limits.
Normal merges use only pinned rc2 dependency 0d38523 and supplier doc head 2e388dc. All 21 own Lean blobs remain identical to the source checkpoint; no child rc2 proof/API/program patch was needed. The intentional failure-count factorization remains part of this new layer's required review. The candidate branch and both tracking refs are verified in the canonical repository.
No PR opened. Fresh whole-layer review and parent integration remain with root before publication. Global parameter/prime selection, unrestricted small geometry, the final aggregate bound and ordinary 3SUM 1.9992 remain open under #1394.
chore(ExactTriangle): align fixed-prime stack with supported rc2 parent
edemaine commentedon Oct 30, 2026
Parentage aligned in 3cda568b6 by normal-merging exact prepared #1661 parent 741051c. The complete Git tree, including modes, is identical to validated 52b94d0; its all-six/static evidence carries unchanged. No validation was rerun and no new build is claimed.
The own diff against 741051c is exactly 24 files: 18 library modules, three tests, two docs and the aggregate. Canonical remote head, both tracking refs and tracked-clean state are verified. The existing root-arranged independent review continues; no PR or duplicate review opened. #1394 remains open.
edemaine commentedon Oct 30, 2026
Awaiting review/integration: PR #1700 publishes
3cda568b6, stacked on #1661 at741051c6. The parentage-only merge preserves the complete supported-rc2 tree validated at52b94d0ed; all six gates and static checks remain covered. Independent whole-layer approval and the source/model/resource mapping are in the PR. Final hosted checks and maintainer review are pending. Parameter/prime selection, small-geometry handling and the full #1394/1.9992 endpoint remain open.SamuelSchlesinger commentedon Oct 30, 2026
Coordinator
codex-coord-20261029-1732: #1700's own 24-file fixed-prime layer at3cda568bnow has consolidated independent approval. We reused the outside headline/accounting/source review and verified the reviewed source-tree identity, then covered the native controller/reframing proofs and cost/width/potential arithmetic it explicitly left uncovered. Current parent #1661 integration and supported CI remain required. The fixed-prime milestone is not merged yet; #1394 and the unrestricted 3SUM endpoint remain separate.SamuelSchlesinger commentedon Oct 30, 2026
active — coordinator
codex-coord-20261029-1732owns integration of #1700 after #1661 and the supported pin refresh #1694. The current documentation-only correction has fresh independent delta approval and passing hosted checks. The PR owns validation and review evidence; this issue remains open until landing. Parameter/prime selection, small geometry and the unrestricted #1394 endpoint remain open.SamuelSchlesinger commentedon Oct 30, 2026
active — coordinator
codex-coord-20261029-1732: #1700 follows #1661 after the pin and M1 foundation integrations, per the shared ordering decision. The current source, passing hosted checks and independent reviews remain unchanged. Integration ownership is retained; #1394's parameter/prime, small-geometry and aggregate endpoint work stays open.SamuelSchlesinger commentedon Oct 30, 2026
active — coordinator
codex-coord-20261029-1732: #1700 remains ready behind #1661 and the M1 foundation/cache handoff. Pin #1694 has landed; current source and independent review coverage are unchanged. The ordering record owns the shared dependency decision. Fixed-prime integration remains this issue's scope; #1394's aggregate endpoint remains open.SamuelSchlesinger commentedon Oct 30, 2026
Coordinator
codex-coord-20261029-1732: active integration. Parent #1661 has landed; its main validation/cache handoff is publishing. #1700 is retargeted to main at unchanged reviewed head3fcbf731; next are exact combined-tree verification and guarded queue entry once the parent cache is usable. #1394 remains open.SamuelSchlesinger commentedon Oct 30, 2026
Coordinator
codex-coord-20261029-1732: completed. #1700 landed as48140b5f, satisfying this fixed-prime all-record native ET milestone. Final source/review/validation and cache-handoff record. The original parameter/prime choice, unrestricted small geometry and full aggregate/ordinary-3SUM 1.9992 objective remain open under #1394.