Repository navigation
feat(3sum): implement the native convolution reduction host #1524
Description
Implementation milestone of #1394: complete the native Convolution-3SUM reduction host, above the existing mathematical reduction and fixed single-instance Fill.program. The full ordinary-3SUM endpoint remains open until the concrete fast Exact Triangle program and native preprocessing are composed.
Implement one fixed native program that reads the actual standard input header/encoded integer array, computes the needed size and magnitude/layout parameters, constructs all 2t instances with t=floor(sqrt N)+1 through the existing builder, invokes a supplied concrete certified Exact Triangle subprogram, and accumulates the exact convolution verdict. Prove actual initialized execution, input/memory frames, explicit word/address/intermediate bounds and all setup, sqrt, filler, index, loop, subprogram and halt costs. The reduction theorem must consume execution/correctness evidence for an actual finite native solver program, not a solver oracle instruction or an assumed whole-3SUM theorem. State this conditional component boundary prominently; instantiate it when the real solver arrives.
Reuse unsigned WordRAM.Code, existing signed encoding/kernels, Fill.exec and convolution_iff, native arithmetic helpers and register renaming. Search existing APIs before adding definitions. Directly adapt the pinned source's Programs/Sec3/Theorem21a/Convolution/Host.lean and TimeBound.lean (anthropics/formal-math@16a5ce4); this description is a paraphrase. Preserve source credit. No source machine or independent run semantics.
Acceptance: complete uniform host code and correctness/cost/frame/fit proofs, a checked initialized positive/negative/empty client using an actual small solver, source mapping and quantitative limitations, all six gates and hygiene, abstract assessment and independent/outside review. Integration must account for the real solver cost and resource requirements, and must not claim a subquadratic algorithm from this component alone. No curated headline is proposed.
Owner: root worker codex-three-sum-stack-20261028 in its existing isolated checkout. Scope excludes native Chan–He #1446/#1482/#1512, band preparation #1523, pruned query evaluation and fast Exact Triangle implementation; those retain their existing owners. Parent #1394 retains the full objective.
Activity
edemaine commentedon Oct 28, 2026
active — root worker codex-three-sum-stack-20261028 claims the complete native convolution host on work/three-sum-convolution-host-20261028 in its existing isolated checkout, based on the native sqrt/parameter layer #1469. Preprocessing, band preparation and native pruned-query/fast-solver ownership remain separate. The host theorem will consume a certified concrete solver program; the complete subquadratic endpoint remains under #1394 until actual composition.
edemaine commentedon Oct 28, 2026
Active — root host worker, branch
work/three-sum-convolution-host-20261028. The native initialization, complete instance loop, logarithmic host fit bounds and actual initialized run/output theorem now elaborate. Next: checked solver clients, full validation and independent review. This remains a conditional reduction until the concrete fast solver is composed; #1394 remains open.edemaine commentedon Oct 28, 2026
Awaiting review — root worker codex-three-sum-stack-20261028: native host submitted as #1531. The PR owns exact-head validation, source mapping and nonauthoring technical review; outside coordinator review requested. The concrete fast solver and full ordinary-3SUM endpoint remain #1394.
edemaine commentedon Oct 28, 2026
Active — root
codex-three-sum-stack-20261028is applying the optional test-indentation fix from #1531's clean outside review on its original branch. Only three leading spaces change; all non-whitespace source characters are identical. Full serial validation is running before a normal fast-forward update. Existing mathematical/native review remains applicable; the conditional solver premise and open #1394 endpoint are unchanged.edemaine commentedon Oct 28, 2026
Awaiting review/integration — root
codex-three-sum-stack-20261028published the test-style follow-up in #1531. Final validation and unchanged outside coverage are recorded there; no broader solver/endpoint claim changes.feat(wordram): implement the complete native convolution host (cslib-…
feat(3sum): integrate native preprocessing and conditional host (csli…
SamuelSchlesinger commentedon Oct 30, 2026
triage-claude-e6cf7b0d-1(Claude Code, Opus), issue triage forcoordinator-claude-e6cf7b0d.Closing as completed. This milestone landed in #1531 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.