Repository navigation
feat(matrix): prove the tensor recursion and pruned evaluation core #1459
Description
Implementation milestone of #1394, following finite modular splitting/recovery #1455. Implement the complete mathematical tensor-recursion core of the thin matrix product algorithm: Schönhage's ten-term polynomial identity with explicit error, recursive full evaluation and tensor coefficient expansion, shared input encodings, pruned evaluation correctness, exact visited-leaf characterization and total passed-set bound. Preserve the exceptional zero-depth/empty-query case rather than claiming unconditional visited-leaf equality.
Use native Cslib placement/namespaces and existing Mathlib polynomial/matrix/finite-set notions; selectively adapt the required definitions and proofs from anthropics/formal-math@16a5ce4, ThreeSumApsp/Sec2/{Lemma6,Recursion,Lemma7_8,Lemma10}.lean and the minimal definitions from PaperStatements.lean. Retain source credit. No source machine or broad statement universe is copied.
Acceptance: all listed core mathematical identities and pruning/count statements, concrete signed/positive/negative/empty-boundary examples, all six validation gates plus hygiene/changed-file lints, precise checked source mapping and quotes, abstract assessment, non-authoring correctness/API review and outside coordinator review request. This milestone gives no native instruction count, fast solver, sparsity-to-saving estimate, or finished 3SUM algorithm. Tiling, sparse leaf bounds, native sparse-product/Exact Triangle code, Convolution host and input/time/width composition, and the improved Section4 route to 1.9992 remain #1394. Native Chan–He preprocessing is independently owned under #1446.
Owner: delegated continuation worker codex-three-sum-continuation-t3-3dda8289, branch work/three-sum-schonhage-core-20261028 in its existing isolated checkout. No competing worker owns this scope.
Activity
edemaine commentedon Oct 28, 2026
active — worker
codex-three-sum-continuation-t3-3dda8289claims #1459 onwork/three-sum-schonhage-core-20261028, based on #1455. Implementing the complete identity/encoding/pruned-evaluation core, with the zero-depth empty-set exception explicit. Native cost/solver claims and the full 1.9992 endpoint remain #1394; native Chan–He ownership remains #1446.edemaine commentedon Oct 28, 2026
awaiting review — worker
codex-three-sum-continuation-t3-3dda8289: #1464 implements the complete identity/full/encoding/pruning core. All six gates, hygiene and changed-file lints pass. Source mapping, exact revisions, initial and delta agent-review evidence and abstract assessment are recorded once in its description. Outside coordinator review requested; keep this milestone open until integration. The full native algorithm remains #1394; next finite thin-product/sparse-bound component is #1463.edemaine commentedon Oct 28, 2026
active — worker
codex-three-sum-continuation-t3-3dda8289resumes #1464 after its inherited header-CI finding. I will restack it after the ancestor fixes, make the small source-wording corrections, rerun six checks and request delta review. Public mathematical meanings and native gaps remain unchanged.edemaine commentedon Oct 28, 2026
active —
codex-three-sum-continuation-t3-3dda8289: #1441/#1445 fixes are pushed; finishing #1455 validation before replaying #1464 and its source-wording nits. The tensor math and tests remain preserved; no native cost or endpoint claim is added.edemaine commentedon Oct 28, 2026
awaiting review —
codex-three-sum-continuation-t3-3dda8289: restacked #1464 at 4f3226c, inheriting the repaired header, and fixed coefficient/API documentation. All six gates and hygiene/changed-file checks pass; evidence and outside delta review request are in #1464. Finite mathematics only; native endpoint remains #1394.edemaine commentedon Oct 28, 2026
active —
codex-three-sum-continuation-t3-3dda8289resumes #1464 for the outside documentation finding. I am rewriting copied comments in the four tensor modules as actual local-API explanations, with unchanged mathematical/program tokens, source credit and scope. The update will fast-forward the original PR branch, with no ancestor restacks, and rerun all six/static gates before publication. Full #1394 remains open.edemaine commentedon Oct 28, 2026
awaiting review —
codex-three-sum-continuation-t3-3dda8289: #1464 now includes the documentation-only repair at 99b8a1b, fast-forwarded on its original branch. It addresses the outside prose finding; all mathematics/program/test bytes outside comments are unchanged. The PR owns final all-six/static, source-identity/quotation and abstract evidence, and the inline finding has a direct reply. Samuel outside delta review requested; root owns refreshed hosted monitoring. No ancestor or descendant remote was restacked. Full #1394 remains open.SamuelSchlesinger commentedon Oct 30, 2026
triage-claude-e6cf7b0d-1(Claude Code, Opus), issue triage forcoordinator-claude-e6cf7b0d.Closing as completed. This milestone landed in #1464 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.