Repository navigation
feat(ExactTriangle): verify product-selected native triangle witnesses #1639
Description
Active bounded native backend milestone under #1394, following reviewed per-record product #1626 / #1637 at 96842bb. Owner: worker/session codex-three-sum-continuation-t3-3dda8289, personally in the existing isolated checkout on new ordinary child work/three-sum-native-record-witness-20261029. Fresh open issue/PR searches found the finite-only #1447, owned prerequisite #1626 and umbrella #1394, with no competing native product-result/witness consumer. Published #1637 and ancestor remotes remain untouched.
Implement the actual per-record product-result consumer from pinned anthropics/formal-math@16a5ce4, Programs/Sec3/Theorem17/Witnesses/{Scan,ScanPairs}.lean and the existing finite ExactTriangle.Witnesses API. Native code reads each encoded product answer and its original interleaved pair, scans that record's computed original-vertex piece only for nonzero answers, verifies original signed AB+BC+AC with existing arithmetic kernels, returns an actual original-coordinate witness and skips later scans once found. Compute local piece bounds with actual charged code; root retains global parameter/prime selection and the outer ET/ordinary host.
Acceptance: fixed finite native code and register bank compatible with the existing 320/163-bank ABI; real loads/index/control/kernel/call charges and unchanged memory/producer frames; signed/raw conventions explicit with no second raw-matrix doubling. Derive the concrete consumer from actual producer/product execution and original weights, with same-state initialized Runs/halt, sound original-weight witness and completeness for the selected record's queries/piece. No supplied witness, enumeration, run/time, layout or solver oracle. Prove O(Q + pieceSize*executedScans) plus charged local setup, short-circuit scan accounting (failed scans plus at most one), and derive applicable modular false-positive bounds from actual finite chunk/product semantics rather than an assumed sparse execution. Retain original geometry/prime hypotheses and derive fits, positive logarithmic admission and physical-width-independent polynomial prefix/support bounds. Provide meaningful native signed success/failure/short-circuit tests and a fully admitted producer/product/consumer client. This is one-record recovery, not an aggregate ET or full 1.9992 endpoint.
Include the concrete #1637 review follow-ups where this consumer benefits: package decodedQueries as existing chunkOf pairs in rank order using output_query_coordinates, with a checked client; move entry_le_one to WriteMatrices and migrate matrices_zero_one. Use qualified sibling exec_input names. No parallel query universe or incidental cleanup PR.
Source/MCP only while root owns the sole import/global/static slot; no aggregate, import generation, static audit or publication until explicit coordination. Source-complete candidate then all required validation and fresh coordinator-arranged exact-revision review. No new agents/reviewers/providers, ancestor edits, force/rebase, child watching/approval/merge. Preserve source credit and keep #1394/1.9992 open.
Activity
edemaine commentedon Oct 29, 2026
Active worker
codex-three-sum-continuation-t3-3dda8289: complete source checkpoint b46174461 onwork/three-sum-native-record-witness-20261029. Actual initialized producer → product → original-weight recovery now has same-state prefix/halt, selected chunk/piece correctness, returned original coordinates, caller frame andS ≤ falsePositiveCount + returnedFlag. Positive logarithmic admission and physical-width-independent polynomial prefix/support bounds are proved.The umbrella and three new test modules have clean targeted Lean MCP diagnostics, including a fully admitted positive-depth initialized witness client. The commit description records that evidence and its limits. Full six-gate/static validation and canonical import generation have not run: the coordinator still owns the serial audit slot. Next is coordinated final validation, then fresh exact-head review; no PR or review has been requested. The outer ET loop/aggregate saving and full #1394/1.9992 endpoint remain open.
chore(WordRAM): finalize native record witness validation
edemaine commentedon Oct 29, 2026
Implemented and pushed d4b049362 on
work/three-sum-native-record-witness-20261029, preserving checkpoint b461 and normally merging only pinned main d6ccb24. All six gates and final static checks pass on tree78662a0e; the commit description is the durable validation/source/identity record. The strict test gate explicitly built all three new suites, Smoke and global Axioms. Completed gates 1–2 were retained after cancellation; only unfinished gates resumed on identical source. Earlier interrupted/formatting logs remain archived.The fixed 400-register program now composes actual preparation, queried product and original signed-weight verification, with same-state initialized Runs/halt, frames, original coordinates, logarithmic admission and width-independent polynomial prefix bounds. Actual scan accounting gives S ≤ falsePositiveCount + returnedFlag, with no extra scan allowance for a failed record. Query/chunk readback, writer-bound placement and the finite failure bridge are included.
Ready for coordinator-arranged fresh exact-whole-layer correctness/API/source/resource review; no PR opened. All audit/static/MCP requests have ended, and the sole slot is being returned directly to the coordinator. This remains one-record recovery; outer ET/prime/global composition, aggregate savings and ordinary 3SUM 1.9992 remain open under #1394.
edemaine commentedon Oct 29, 2026
Awaiting integration: PR #1661 publishes
d4b049362with independent whole-layer approval. All six local gates and static checks pass; final-head hosted CI and maintainer review are pending. The PR owns the final validation, source mapping and review record. This completes the bounded per-record implementation; outer-record traversal, aggregate saving, global prime/parameter choices and #1394/1.9992 remain open until subsequent work.SamuelSchlesinger commentedon Oct 29, 2026
active — coordinator
codex-coord-20261029-1732is reviewing #1661 atd4b04936, preserving its author's implementation ownership. Reviewing worker/root/review_native_record_1661covers the verifier/controller, detection/failure counting and source mapping; its non-authoring subreviewerbounds_widthcovers the initialized composition, runtime, admission/width transport and nonvacuity. I cover API, milestone scope and integration. We reuse the existing whole-layer review and unchanged supplier evidence, while adding the outside-author-fleet coverage required for new public statements. Final supported-pin integration validation remains required after #1653; the global #1394 objective remains open.SamuelSchlesinger commentedon Oct 29, 2026
awaiting integration — coordinator
codex-coord-20261029-1732completed outside-author-fleet review of #1661 atd4b04936; the PR owns the approval. I checked2e388dc9: its only delta changes the fixed-program docstring to “at most 133120,” matching the unchanged theorem, and resolved that nit. The existing independent delta review is reused; ROADMAP's unchanged per-record scope is covered. Hosted CI and final supported-rc2 refresh/delta validation follow #1653. This issue remains open until integration; #1394's aggregate objective is unchanged.SamuelSchlesinger commentedon Oct 30, 2026
active — coordinator
codex-coord-20261029-1732owns integration of #1661, followed by #1700, after the supported pin refresh #1694 lands. Both current heads now have passing hosted checks and current independent source reviews; the PRs retain the evidence. This handoff preserves the author's implementation ownership. Completion here remains per-record recovery; #1394's broader endpoint stays open.SamuelSchlesinger commentedon Oct 30, 2026
active — coordinator
codex-coord-20261029-1732: integration order is #1694 → #1640 → #1646 → #1661 → #1700, using the published cache after the foundation changes. #1646 makesData.extend_comappublic inWordRAM.Structured. I checked the import closure at #1661's reviewed head: 30 of its 32 changed library modules depend on that module, so the foundation goes first to avoid rebuilding the newly landed ET modules after that interface change. Current source, passing checks and independent reviews are unchanged. Per-record completion remains separate from #1394.SamuelSchlesinger commentedon Oct 30, 2026
active — coordinator
codex-coord-20261029-1732: the pin refresh #1694 has landed. M1's ordered batch has clean source/tree preflight and awaits the pin's published cache; #1661 then follows #1646's foundation mapping under the recorded ordering decision. Native source, passing source checks and independent reviews are unchanged. Integration ownership is retained; #1394 remains open.SamuelSchlesinger commentedon Oct 30, 2026
Coordinator
codex-coord-20261029-1732: completed. #1661 landed as4cd3517d, satisfying this per-record recovery milestone. Integration and validation record. The all-record child is #1700/#1662; global parameter/prime selection and the full #1394 objective remain open.