Repository navigation
feat(ExactTriangle): implement native cyclic-Strassen modular counting #1701
Description
Owner: implementation worker/session codex-three-sum-continuation-t3-3dda8289, personally on ordinary child work/three-sum-native-modular-counter-20261030 from #1700 exact 3cda568, in the existing isolated checkout. Fresh searches for Strassen, CountPrime and cyclic/modular counters found no competing native implementation. #1442 supplies finite mathematics only. Published supplier branches remain frozen.
Implement the concrete native modular triangle counter needed for deterministic prime selection under #1394. Root retains prime enumeration/argmin, global D/g/m selection and ordinary outer-host/final 3SUM composition.
Acceptance is the complete pipeline from original canonical-signed AB/BC/AC arrays and runtime positive p: actual residues; cyclic-coefficient monomial matrices and padding/index tables; seven-product Strassen recursion with an explicit native stack and all ring coefficient arithmetic; coefficient extraction and sum equal to existing ExactTriangle.countZeroMod. No supplied multiplication, convolution, table/layout, answer, execution or time contract. No cubic triple enumerator substituted for the required algorithm.
The fixed finite native program must preserve original arrays/caller prefix, handle dirty workspace, prove original-input fits and positive logarithmic admission, width-independent polynomial prefix/support, actual initialized or caller-safe execution, and charge every coefficient operation, memory/index/setup/copy/recursive call/return/control/halt. Derive subcubic-in-n and polynomial-in-p cost from the actual program and provide complete small native count examples plus the general correctness/resource theorem.
Pinned source: anthropics/formal-math@16a5ce4, 3sum-apsp/ThreeSumApsp/Programs/Sec3/Theorem17/Hashing/{CountPrime,RingOps,Strassen,StrassenTime,ZOrder,Count}.lean and the corresponding finite specifications. The source charges quadratic cyclic convolution: strSteps p 0 = 32pp+21p+16; strSteps p (j+1) = 7strSteps p j+696*(4^j*p)+900. These Light constants do not automatically become native bounds. Native instruction costs must be proved directly. Preserve Anthropic source credit and the existing quotient-ring/problem APIs.
Reuse search found existing CyclicIntRing, coefficient-count identities, signed arithmetic, residue loops, copy/power/log and explicit-stack patterns, but no native cyclic convolution or Strassen implementation. The first internal prerequisite is executable cyclic coefficient arithmetic: finite vector/quotient meaning, actual signed coefficient add/subtract and O(p^2) cyclic multiplication, with explicit disjoint blocks, frame/fits/cost and nonzero signed examples. This is a useful independently deliverable kernel if the stack needs splitting; it does not complete this counter issue, and no kernel contract may be assumed in the final counter. Subsequent native stack/matrix preparation/count extraction remain part of this issue.
Source/MCP only until root explicitly hands over the sole import/global/static audit slot. No aggregate/import generation/static run, PR/publication, new agent/provider/reviewer, ancestor edit, force/rebase, watch/approval/merge. Required final validation and root-arranged fresh review precede submission.
The full counter objective, deterministic fast prime selection and ordinary distinct-position 3SUM 1.9992 remain open under #1394. Fixed-prime solver correctness in #1700 does not itself supply fast selection. No curated headline/abstract promotion is planned. AI assistance: OpenAI Codex.
Activity
edemaine commentedon Oct 30, 2026
Active bounded extraction by worker/session
codex-three-sum-continuation-t3-3dda8289, branchwork/three-sum-cyclic-kernel-20261030from pinned mainf15b07e7f. Scope is only the completed six-module native cyclic-convolution kernel and its initialized execution tests, extracted from local14e4ba5bb; fresh searches found no competing kernel PR. Full counter checkpoint4419dca359and its resume note remain preserved and paused.This is an independently useful prerequisite within #1701, not completion of its counter criteria or #1394/1.9992. Targeted validation and one root-arranged exact-source review precede publication; hosted exact-head CI may supply the six gates. I will hand off the pushed candidate and pause again.
edemaine commentedon Oct 30, 2026
Kernel prerequisite candidate: 671ccbf648, main base
f15b07e7f. Only six exact kernel library files, initialized/alias tests, canonical imports and concise scope docs are included. The full counter checkpoint4419dca359stays preserved and paused; #1701/#1394 acceptance remains open.Static/source/import checks pass. The original extracted kernel had clean targeted MCP/tests; the current-main check was stopped in cold dependency preparation after cache extraction permissions failed. No new-head Lean/all-six or new alias execution success is claimed; hosted exact-head CI remains required. Commit description records the bounded evidence and gap.
Handed to root for one fresh whole-kernel review and eventual PR; no PR opened by this worker. User-requested pause resumes now, and the sole audit slot returns directly to root.
edemaine commentedon Oct 30, 2026
Paused after publishing the bounded cyclic-convolution prerequisite as PR #1713. Source/API review is clear; exact-head hosted CI is still required. Full #1701 and #1394 remain open.
The unfinished Strassen/counter work is now available at checkpoint
4419dca359, branchwork/three-sum-native-modular-counter-20261030. It has targeted checks only, not final validation or independent review. It preserves all-depth native Strassen execution and matrix preparation/readback proofs. Next: selected-coefficient scan/count extraction, complete initialized counter composition, and original-input width, prefix/support and charged subcubic bounds. No further implementation is active.SamuelSchlesinger commentedon Oct 30, 2026
Active integration only — non-authoring coordinator
codex-coord-cyclic-1713-20261030owns the approved #1713 handoff at671ccbf648802beac6a1c2f649db4625f09b365a. I will preserve its reviewed kernel/test payload and current main, use a guarded tail enqueue, and follow actual landing plus a usable descendant-main cache handoff. The larger counter implementation remains paused/preserved; #1701 and #1394 stay open.SamuelSchlesinger commentedon Oct 30, 2026
Coordinator
codex-coord-20261029-1732: integration handoff for the landed #1713 cyclic-kernel prerequisite. I now own its active main/cache run41019268001; single integration record. The source implementation remains paused as previously recorded, and the full #1701/#1394 objectives remain open.feat(WordRAM): add native cyclic coefficient multiplication (cslib-co…
edemaine commentedon Oct 31, 2026
Active again: worker/session codex-three-sum-continuation-t3-3dda8289 resumes the complete counter from preserved
4419dca359on ordinary branchwork/three-sum-native-modular-counter-resume-20261031. The landed #1713 kernel is reused; next are actual selected-coefficient scan, full initialized/caller-safe composition, and original-input width/support/charged subcubic bounds. Counter ABI remains128 registers, arguments64–69 and raw result70 for #2098. Root retains selection/global parameters/outer host. Source/MCP stage only; full #1701/#1394 acceptance remains open.feat(WordRAM): compose the complete native prime-selector loop
edemaine commentedon Oct 31, 2026
Complete counter source checkpoint: 61c82f668. It now proves original caller and initialized same-state prefix/halt correctness, exact raw modular count, original/dirty-workspace frames, logarithmic source admission, width-independent polynomial prefix/support and the fully charged
3704*(p+1)²*(n+1)^2.81bound. The p factor is explicit. Targeted MCP source and meaningful initialized/alias/padding tests pass; step counts in the clients are upper bounds.Final canonical imports/static audits, exact-head six-gate coverage and one fresh whole-layer nonauthoring review remain before publication/integration. I have requested the next coordinated import/static slot; no PR or review was opened by this worker. #1701 awaits validation/integration; prime selection #2098 and the full #1394/1.9992 objective remain open.
edemaine commentedon Oct 31, 2026
Independent non-authoring agent
/root/countprime_review, with a separate narrow bounds/width audit: approve source/API at61c82f6689d8c146d334c2e84fdc1974564f2e37. No blocking findings. This is agent review, not human or platform approval. Final canonical imports/static checks and exact-head six-gate CI are still required before integration.The review inspected the complete finite/native counter layer, original-input/caller contracts, real seven-child stack recursion, signed array aliasing, dirty workspace, magnitude/address frames, coefficient extraction into existing
countZeroMod, same-state initialized prefix/halt, charged time and width-independent prefix/support proofs, and all four test suites. The n exponent2.81 is subcubic, with the quadratic runtime-p factor explicit. All eight pinned source hashes and the exact countOf_eq quote/locator were independently verified; unchanged #1713 kernel coverage was reused only after blob checks. No new abstract/catalogue impact.Two optional locator nits will be corrected before publication: finite Strassen/Defs recurrence81–96 and Correctness identity/proof105–126. No native definition, mathematical statement or proof change is requested. Full #2098 selection, global host/parameters and #1394/1.9992 remain open.
chore(ExactTriangle): register complete native modular counter
edemaine commentedon Oct 31, 2026
Complete #1701 counter candidate 7bc9b1cb099ee87fee036a2d656c6c78497f7e03 is ready for root-arranged review/publication. Final tree
86adfee5059525784da6cfba4125e6382131a683adds only 67 canonical imports to source checkpoint 61c82; no implementation/proof/test source changed during final audit.Strict scoped compilation of all 69 changed library modules/four tests, complete changed-module and test environment lint coverage, canonical imports, hygiene/simp, scoped changed-file checks, strict body names and full-diff/source identities pass. Exact coverage and preserved resource/artifact dispositions are in the commit. Hosted exact-head CI must supply all six before integration; no local all-six claim.
Fresh whole-layer review is underway under root. Root will apply the two reserved locator-only doc corrections afterward. No PR opened by this worker. This computes actual modular counts; prime selection #2098 and full #1394/1.9992 composition remain open. Sole audit slot is returned directly to root after final handoff; no further source work pending findings.
doc(Strassen): correct pinned recurrence and identity locators
edemaine commentedon Oct 31, 2026
Awaiting review/integration: PR #2109 publishes the complete native counter. The PR owns final validation/review evidence; exact-head hosted six-gate CI is running. Both source-reference nits are fixed and independently reviewed. Prime selection #2098 and the full #1394/1.9992 endpoint remain open.