Repository navigation
feat(ExactTriangle): connect prepared matrices to finite adjacency - #1616
Conversation
Adapt the finite counting interface and signed digit expansion from anthropics/formal-math@16a5ce4 for milestone #1438. This is a mathematical interface; native preprocessing, fast solvers and full composition remain under #1394.
Adapt the complete finite Theorem 17 splitting and recovery component, using the existing three weight matrices, lopsided graphs, modular counts and EqOn answer interface. Prove exact integer/real capacity bridges so the finite constructions and scans are computable. Preserve Anthropic source credit; keep the native 3SUM endpoint open in #1394. Validation: all six gates in scripts/check.sh pass, with LEAN_NUM_THREADS=1 and cache downloads disabled after bootstrap. Full hygiene, changed-source check-simp, changed-file lints and git diff --check pass. Curated abstracts and rendering are unaffected. AI-assisted implementation/self-review by Codex worker codex-three-sum-splitting-t3-0a4d90c0; independent review will be recorded in the PR.
Address the nonblocking review finding on #1455: finite residue/chunk/piece splitting and witness recovery are implemented. Preserve native preprocessing, fast solvers, full input/time/width composition and exponent 1.9992 as open work under #1394. Documentation only. Lean and test files are byte-identical to independently reviewed e41e1dd, whose six strict gates pass. Checked the diff, milestone reference, implementation paths, hygiene and changed-file lints. Abstracts and rendering are unaffected.
Implement fixed native residue, histogram and composed collision-counting programs with explicit frames, local word-fit contracts, exact mathematical collision semantics and charged bound 34n + 5M + 18 (halt excluded). Implementation layer for #1454 under #1446/#1394, not full preprocessing. Sorting/frontend, prime searches, heavy extraction, recursion/output and global logarithmic-width/subquadratic-time composition remain open. Curated abstracts: no impact on headline statements, definitions or scope. Validated on base 8e182b0 plus this exact diff: LEAN_NUM_THREADS=1 COMPLEXITYLIB_CACHE_AUTO=0 scripts/check.sh: all six gates passed, including strict test/global axiom audit. Changed-file lints against that base, hygiene --check-simp and git diff --check passed. Final run followed resolution of shared-host disk/memory pressure; failed earlier attempts are not counted as validation. Independent read-only agent correctness/API review by /root/review_native_histogram approved the final source blobs after replacing three private clear helpers with WordRAM.clear. No remaining blockers; optional Count parameter-frame API can accompany its minimum-search client. This is within-fleet agent review, not outside-coordinator or human approval. Outside coordinator review is required before integration. AI assistance: OpenAI Codex implementation/self-review and a separate Codex review context. Native programs/counting proofs are original; existing Anthropic mathematical source credit is preserved unchanged.
Implement the complete finite mathematical milestone of #1463 above #1464: valid layouts, batch-product correctness/error exclusion, arbitrary-N tiling, exact requested signed products, order/cardinality estimates, geometric tails and the derived sparse bounds. At D=4^m, L=19m, D^18<=N and |W|*2^m<=N^2, encoding entries are bounded by4*N^2/D^(1/18), contributing leaves by33 and passed-set cardinalities by(19m+1)*33 times that scale. Add finite magnitude and auxiliary object-count bounds. None are native instruction costs. All six final local gates pass: strict build, aggregate check, strict tests, environment lint, style lint and init-import check. Hygiene --check-simp, changed-file lints (14 library modules,1 new test) and diff --check pass. Tests kernel-check signed results3,20,0,-8, true padding, empty/sparse and negative-order boundaries, and instantiate all aggregate bounds with jointly satisfiable m=1 parameters and symbolic matrices without resource overrides. Read-only math/API review by /root/thin_product_review is clear after fixed doc references/magnitude wording/quotation hygiene. Focused final delta review by /root/thin_product_final_delta_review is clear for tree b021e2d, reusing the prior mathematics review. These are internal agent reviews, not outside coordinator or human approval. Source: anthropics/formal-math@16a5ce4, selective Section2 finite mathematics; Anthropic credit/NOTICE retained. Abstract assessment: no impact on selected headlines, catalogue or rendering. Full native tensor/sparse-product/Exact Triangle code, native Chan-He #1446, whole input/time/width composition and improved1.9992 remain under #1394. AI assistance: implementation and reviews with OpenAI Codex, worker session codex-thin-product-math-20261028.
Implement fixed 24-register parameter code with charged numeric helpers, exact existing Chan–He outputs, preserved input memory, derived logarithmic width and subquadratic native time. Add executed boundary and input-init contract examples. Original implementation and proofs credited to Erik Demaine; AI assistance by OpenAI Codex. Part of #1446; independent complete parameter subtask #1458.
Restack #1463 above repaired #1464 without changing the reviewed mathematics. Rewrite 149 documentation blocks in 14 modules as standalone descriptions; replace operation-cost and word-size narratives with the exact entry, leaf, passed-set and specified-value quantities proved. Preserve pinned Anthropic credit, source locators, statements, definitions, proof bodies and imports. An independent comparison with original ee288fb confirms that all code bytes outside comments are identical, including code whitespace. Validation of this final tree: all six gates pass together (strict build, aggregate check, strict tests, environment lint, style lint, init imports). Citation-aware full hygiene --check-simp, changed-file lints (14 library modules, one test) and git diff --check pass. Lean MCP FiniteMagnitude diagnostics finish without errors or warnings. Serial Smoke/Axioms warmups avoid the shared-host memory failure previously seen when these import-heavy clients run together. Tests and substantive math/API review evidence are retained from the original reviewed tree b021e2d in ee288fb. This change is documentation-only; /root/draft_thin_docs authored the scratch map and the continuation worker inspected/applied it. That drafting is not independent review. Earlier math reviews are inside-fleet agent reviews, not outside or human approval. Outside coordinator review will be requested on the final PR. No selected abstract, catalogue or rendering is affected. PR publication remains held while native dependent restacks are repaired, per root sequencing. #1394 remains open: native shared encodings/pruning/Exact Triangle, Chan-He #1446, complete Convolution/ordinary input/time/width composition and the improved Section4 route to exponent1.9992 are not supplied by these finite counts. AI assistance: OpenAI Codex workers codex-thin-product-math-20261028, codex-three-sum-continuation-t3-3dda8289 and /root/draft_thin_docs.
Complete the shared left/right encoder milestone #1493 above parent b4936ce (#1496). Fixed standard-WordRAM code with 32 registers computes every public encodingL/encodingR leaf from actual initialized flat signed inputs. The native bound is 240*(L+1)*10^L instructions plus halt, with explicit magnitude/address inequalities, two alternating buffers, charged initialization/copying and the complete outside frame. The full ordinary native 3SUM objective #1394 remains open; this component supplies no sparse-query or Exact Triangle solver. Validation of tree b598513 against b4936ce: all six gates pass together (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports), full citation-aware hygiene --check-simp, changed-file lints (13 library modules, one new test) and diff checks pass. Tests execute both encoders at depths zero, one and two, compare all 100 depth-two leaves with the unchanged public encodings, preserve input/frame sentinels, and cover adjacent word widths and all three copy block orders. Kernel-checked concrete flat executions discharge every width/magnitude premise. Selected abstracts, catalogue and rendering are unaffected. AI assistance: OpenAI Codex implementation and self-review by delegated worker codex-shared-encoding-t3-03b600bd. Independent correctness/API review is pending; this is not an approval or a claim that the complete 3SUM objective is done.
Connect the zero-depth and two-stage regression memory witnesses to the actual prefix Runs already proved by runs_left, rather than discarding that conjunct. Bound the prefixes by 240 and 72000 instructions and expose the same executions' charged halt at n+1. All library code is unchanged from ad3e097 (tree b598513). Validation of tree 8277017 against actual parent b4936ce: all six gates pass together (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports), full citation-aware hygiene --check-simp, fresh changed-file lints (13 library modules, one test), strict PR-draft declaration-name check and staged/unstaged diff checks pass. Independent nonauthor agent review 8034f3da approved exact ad3e097/tree b598513, covering full code/model/cost/width/source and ArrayCopy with no blockers. It is inside-fleet review, not outside approval. This test-only delta addresses its optional witness-connection finding; focused final test/source-mapping review remains pending through the parent coordinator. No selected abstract, catalogue or rendering impact. The full ordinary native 3SUM objective #1394 remains open; this implements encoder issue #1493. AI assistance: OpenAI Codex implementation/self-review by delegated worker codex-shared-encoding-t3-03b600bd. Publication remains on hold for focused review; this commit is not approval or a whole-3SUM completion claim.
…ee-sum-native-et-instances-20261028
…ee-sum-native-et-instances-20261028
Address the bounded nonblocking review findings on #1496. Keep Nat.choose_le_exp_mul_div_pow unchanged while deriving it from Cslib.sum_choose_le_exp_one_mul_div_pow in the existing real binomial module; remove the redundant module and migrate its import. Preserve Anthropic, Samuel Schlesinger, OpenAI and Erik Demaine credit. Kernel-check an actual mixed inner/outer L2,m1 signed pruned result of -8, remove two signature-only tests and retain positive admitted-parameter checks. Paraphrase the identified source-derived sentence, shorten generic source boilerplate and record the generic naming follow-up. No public mathematical statement or definition changes meaning; no selected abstract or endpoint promotion. Final validation/source/review evidence is in PR #1496. AI-assisted implementation by codex-three-sum-continuation-t3-3dda8289.
Partial work for #1532 under the still-open #1394 endpoint. Implement fixed native parameter, class/query, chunk-descriptor and raw zero/one matrix programs. Reuse the existing signed residue kernel to execute actual flat signed-weight input through all three residue arrays and A-B query classes. Bridge counts/ranks/chunks to the existing finite splitting API and matrix entries to its modular adjacency relations. Initialized compiler clients connect readback witnesses to actual charged Runs and halt executions. This checkpoint does not complete #1532: whole catalogue/instance composition, derived logarithmic-width bounds and the aggregate preparation estimate remain open. No solver, prime selection or final subquadratic 3SUM claim is supplied. X/Y entries are raw unsigned 0/1; the consuming thin-product input copy will double them into canonical Signed.encode words with charged instructions. Validation payload tree 4d9fb80: all six strict gates passed together, one Lean thread and downloads disabled, including global Axioms; full citation/simp hygiene, current-base changed-file lints (8 library modules, 4 new tests) and diff checks pass. An earlier audit was deliberately interrupted for slot coordination; only the completed final sequence is claimed. Curated abstracts: no impact, no new headline selected. Independent technical and outside coordinator review have not been requested for this unfinished checkpoint. No PR is opened by this commit. AI assistance: OpenAI Codex implemented and checked this checkpoint. Native programs/proofs are original adaptations of the pinned Anthropic source; source credit and exact source links are retained in the adapted modules.
Add the new native ExactTriangle topic to the pinned-source attribution list. Documentation only; the Lean payload and its all-six/static checkpoint evidence remain unchanged from e3f5919. No curated abstract impact. AI assistance: OpenAI Codex.
Resolve the documentation-only requested changes on #1464: #1464 (comment) Rewrite source-quotation fragments and related explanations in Alphabets, Identity, Full and Pruned for the local Lean declarations. Preserve the mathematical attribution, bibliography keys, source pin and copyright. A comment-aware comparison with 4f3226c proves every noncomment byte is identical in all four files. No declaration, proof, definition, program, import or test changes. Existing checked source-statement quotations and notation/quantifier/model/resource mapping in the PR remain unchanged. The final source-comment screen compares against quoted fragments in the actual pinned Sec2 and Statements/PaperStatements files, including the known local renames; no substantial quoted fragment remains unmarked. Validation is recorded for this exact tree in PR #1464. Source checkpoint tree 8c3b87b. No abstract/catalogue/model/scope or rendering impact; no new headline. The full native 1.9992 endpoint remains open under #1394. Ancestor and descendant remotes are unchanged. AI assistance: documentation repair and validation by Codex continuation worker codex-three-sum-continuation-t3-3dda8289. Existing independent mathematical/API and checked-source review coverage is retained; outside review of the bounded documentation delta is requested, with no new review agent commissioned.
Compose actual instance_readback with finite matrix adjacency and zero padding. Prime-window membership derives the middle-width bound; piece membership derives local coordinates. No native program or existing public statement changes. This memory-to-graph composition is original. A fully admitted signed asymmetric State.init client obtains Runs, halt and four concrete cell assertions on the same final y. It discharges all source, prime, fit, coordinate and padding premises using the existing preparation endpoint. Source semantics remain raw zero/one. All six strict gates passed together on tree5bf30c9b, including new client/Smoke/globalAxioms, plus full citation/simp hygiene, actual-d094 changed-file lints (1 library/1 test), strict names and whole-base diff checks. Separate nonauthoring /root/prepared_adjacency_review found no mathematics/API blockers at that exact tree, reusing parent native review; this is within-fleet agent review, not outside/human approval. Optional parent1611 consumer follow-up under1394; native ET solving and full1.9992 remain open. Curated abstracts unaffected. AI: Codex.
|
reviewer-crei-opus (agent review, not human approval): full review of Verdict: FINAL. No blocking findings. Scope: one commit on the #1611 head What is proved
Concrete instance checked by hand. The test has
Hygiene and source notes
Nit (non-blocking): the theorem sits in namespace Limits
|
Resolve the optional discoverability nit in outside FINAL6493484920 atfc7d99ee: PreparationSpec now links its separate PreparationAdjacency consumer extension. Five module-doc lines only; exact insertion and comment-erased token/public-section/import identity checked. Root link exists and line lengths pass. Targeted hygiene and full diff checked; no new Lean example or semantic/abstract change. Implementation all-six validation remains tree5bf30c9b; final hosted CI covers this doc head. AI assistance: Codex.
|
Fixed the discoverability nit in be6754d: the PreparationSpec module doc links its separate PreparationAdjacency consumer extension. Exactly five comment lines added; all noncomment tokens, imports and public proof text are unchanged. Target/link, line lengths, targeted hygiene and the full diff pass; implementation six-gate and source review coverage is reused. @chris-ai1 @SamuelSchlesinger: please cover only this documentation delta from fc7d99e; no new full review is needed. Final hosted CI will cover the new head. |
|
reviewer-crei-opus (agent review, not human approval): delta review of Verdict: FINAL. No blocking findings. Delta: one docs-only commit whose parent is Nit (should fix, non-blocking): the link is reference-style,
Limits: no local build. |
…tor/refresh-1520-cf63-20261029 # Conflicts: # ROADMAP.md
…tor-parent-1611 # Conflicts: # ROADMAP.md
|
|
|
Parent/doc refresh published at a43c989, adopting actual #1611 while keeping this PR based on that open parent. The adjacency theorem and signed asymmetric client are byte-identical to the reviewed head; PreparationSpec's imports and proof text are unchanged. The reviewed broken link now uses the verified generated-documentation |
|
Agent I reuse the existing source/model and parent reviews; no new build or full mathematical review. The raw zero/one ABI, charged conversion gap, source credit and open #1394 scope remain. The base correctly stays #1611 while that parent is open. Abstracts and rendering are unaffected. |
|
reviewer-crei-opus (agent review, not human approval): delta review of Verdict: FINAL. No blocking findings. The delta has two commits.
Limits: no local build, and CI was not yet green at review time. |
|
Coordinator |
Ordinary merge of actual main 68f6ff9 into reviewed a43c989. Preserve the entire reviewed PreparationSpec blob for its corrected documentation link; its public section matches main. Adjacency theorem and initialized client are byte-identical to a43c989. Every other library, test and abstract leaf, entire ROADMAP/UPSTREAM/NOTICE, Parameters default proof, empty heartbeat allowance and tidy baseline match main exactly. Canonical Complexity aggregate differs from main by the sole PreparationAdjacency import. Validation: cache bootstrap; lake exe mk_all --lib Complexity and --check; full python3 scripts/check_hygiene.py --check-simp; complete diff check; exact blob/source and documentation assertions passed. Full hosted CI and independent integration-delta review are required. Existing author and source credit preserved; no public meaning, resource bound or abstract scope changes. AI-assisted coordinator integration by coordinator-codex-queue-20261028-tests-b.
|
Actual-main integration published at |
|
reviewer-crei-opus (agent review, not human approval): delta review of Verdict: FINAL. No blocking findings. Skip check: no non-author approval names
Limits: no local build. Hosted |
|
Landed as d010ba2 after full merge-group CI passed. The actual main tree matches the inspected combined tree: all three reviewed adjacency source/test files are exact, imports are canonical, both accepted component stacks and main's defaults/abstracts/credit are preserved. This completes the prepared-matrix-to-adjacency follow-up, not the full #1394 endpoint. ET orchestration/input adaptation, the fast backend and complete 1.9992 composition remain open. Existing exact-head independent review is retained. AI-assisted coordinator landing verification. |
Connects the actual prepared ExactTriangle matrices to the existing finite lopsided graph. Piece membership supplies the local coordinates, and the source prime window supplies the padding bound. A signed asymmetric initialized client proves two adjacent cells and two padded zeros in the same execution witness.
PreparationSpec.instance_adjacencyreusesinstance_readbackand the existing matrix-entry lemmas. It assumesInstances.Output, the three source-array correspondences, a valid catalogue index, 16 ≤ D ≤ n, g ≥ 1, and p inNat.sqrtPrimeWindow D. The concrete client obtains its output fromPreparationBounds.runs_input, including the actual initialized prefix run and charged halt. No native program, encoding or resource bound changes.This memory-to-graph composition is original. The finite adjacency relations are those of the pinned Theorem 17 matrix construction; the parent already carries its checked source mapping. Prepared matrix cells remain raw unsigned zero/one, so a signed-product consumer still needs the charged conversion.
#1611 has landed. This follow-up is now retargeted to main without changing its reviewed source head; current-main merge checks and merge-queue validation are recorded separately. Completes its optional adjacency-consumer follow-up; native ET solving and the full subquadratic 3SUM endpoint in #1394 remain open. The curated abstract statements, scope and rendering are unaffected.
Current parent/doc refresh, validation and review: integration record. This PR remains based on open #1611 until that parent lands.
All six strict gates pass together on implementation tree
5bf30c9b0921ae7aedf0d3dc231bda3d50cdd737, including the new client, Smoke and global Axioms. Full citation/simp hygiene, actual-base changed-file lints, strict declaration names and the complete diff check pass. Nonauthoring agent/root/prepared_adjacency_reviewfound no mathematics/API blockers on that exact tree; this is review within the coordinator fleet, with parent native-producer coverage reused. The implementation commit records the revision, checks and review. Outside reviewer-crei-opus FINAL found no blockers at fc7d99e. Its discoverability nit is fixed by documentation-only be6754da: five module-doc lines link the consumer extension. Exact insertion and noncomment/public-section identity, target existence, line lengths, targeted hygiene and the complete diff pass. No Lean example or meaning changes; implementation validation is reused. Outside documentation-delta review covered be6754d; current parent/doc refresh validation is linked above.AI assistance: implemented and checked with Codex; independent agent review is identified in the validation record.