Repository navigation
feat(exactTriangle): prove modular counting and the selected-prime bound #1442
Description
Mathematical milestone of #1394, following #1441's lopsided matrix interface. Owner: delegated continuation worker codex-three-sum-continuation-t3-3dda8289; planned branch work/three-sum-modular-hashing-20261028 in the provided isolated checkout.
Adapt the complete counting/prime-selection step from anthropics/formal-math@16a5ce4, ThreeSumApsp/Sec3/Theorem17/Hashing.lean, together with the required finite-prime-window estimate. Reuse the existing three-matrix HasZeroTriangle predicate; do not copy TriangleInstance or a source machine/problem universe. Prove modular count = true zero count + false positives, the cyclic-polynomial matrix coefficient identity, existence/minimality of a prime in [sqrt(D)/2,sqrt(D)), and the uniform false-positive bound for 16≤D≤n and polynomially bounded integer weights. Preserve source/Mathlib credit.
Acceptance: all of those finite mathematical statements, explicit hypotheses/quantifiers, satisfiable positive/negative/boundary examples, all six checks/hygiene, abstract assessment and independent/coordinator review request. This is no native preprocessing or solver-time certificate.
Residue/chunk/piece splitting and witness recovery, tensor/sparse-query programs, native Chan–He preprocessing, native Exact Triangle and complete host/input/time/width/asymptotic composition remain under #1394, including the improved Section4 route to exponent 1.9992. Completing this bounded milestone must not close or narrow that endpoint.
Activity
edemaine commentedon Oct 28, 2026
active — worker
codex-three-sum-continuation-t3-3dda8289claims #1442 onwork/three-sum-modular-hashing-20261028, based on #1441 plus the updated #1437 base. Scope is the full finite modular count/coefficient/prime-selection/false-positive-bound step. I will use plain supplied weight matrices and the existing HasZeroTriangle predicate; native programs, splitting and the full #1394 endpoint remain separate.edemaine commentedon Oct 28, 2026
awaiting review — worker
codex-three-sum-continuation-t3-3dda8289: #1445 implements the complete finite count/coefficient/prime-selection step with all-window bound. All six gates, hygiene and changed-file lints pass; final source mapping, edge cases, revision and review limits are recorded once in its description. Outside coordinator review requested. Keep this milestone open until integration; native preprocessing, splitting/solver/composition and exponent 1.9992 remain #1394.edemaine commentedon Oct 28, 2026
active — worker
codex-three-sum-continuation-t3-3dda8289resumes #1445 onwork/three-sum-hashing-fix-3dda8289after #1441’s requested rebase. Fixing the PrimeWindow copyright header and rewriting the affected public docstrings in Lean terms, preserving attribution and mathematical statements. All six checks and a fresh review request follow.edemaine commentedon Oct 28, 2026
awaiting review —
codex-three-sum-continuation-t3-3dda8289: #1445 now has the single-line copyright header, self-contained public docstrings and the updated base. All six local gates and the forced header-linter check pass; final evidence and a fresh review request are in the PR.SamuelSchlesinger commentedon Oct 30, 2026
triage-claude-e6cf7b0d-1(Claude Code, Opus), issue triage forcoordinator-claude-e6cf7b0d.Closing as completed. This milestone landed in #1445 on 2026-10-29, and that PR records the validation and review against the acceptance criteria above. The broader native ordinary-3SUM endpoint (exponent 1.9992) stays open in #1394.