Repository navigation
feat(ExactTriangle): bound initialized native ET by natural subcubic time - #2154
Merged
SamuelSchlesinger merged 173 commits intoNov 2, 2026
Merged
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.
Work in progress for #1526. Fixed native controller and initialized-input interpreter regressions, numerical child-set bridge, call-count potential, charged power/scan/clear/frame/arithmetic/return kernels. Individual current Lean modules have clean MCP diagnostics; the earlier strict targeted scan/count/value/test checkpoint passed. The complete global controller invariant, native evaluator theorem, actual initialized flat-run clients and sparse charged bound remain unfinished. No full six-gate or independent review claim; no PR submission. Full #1394 endpoint remains open. AI-assisted implementation by codex-three-sum-continuation-t3-3dda8289.
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.
Implement the complete bounded #1523 native component under #1394. A fixed 96-register standard WordRAM program computes valid subset/inverse tables and a deterministic existing Layout, prepares all padded signed row/column bands, calls the unchanged #1520 encoders once per shared band, collects every leaf, and restores the entire initialized input prefix and outside frame. The State.init and flat Runs/Executes clients bind the actual output memory to public encodingL/R in the unchanged leafIndex order (P0 digit 9). All powers, mask/popcount/root/table loops, indices, guarded matrix addresses, initialization, copying, encoder calls, loop controls and halt are charged. The generic bound is 4096*(L+1)*(1+N*4^m+2^L+2*numBands*10^L), plus halt; at L=19m and N>=(4^m)^18, the full charged run is <=81920*(L+1)*N^2/(4^m)^(1/18). Width assumptions are explicit original-parameter inequalities: the wordBudget fits target w+2 and 7^L*A < 2^(w-1), w>0, A>=0. Actual signed kernels use at most 15/17 instructions for add/subtract, already included through the unchanged encoder's real cost. No all-state fit, callback, solver, assumed run/cost or source machine semantics is a hypothesis. Symbolic positive-depth thin native examples and concrete signed/padded/frame/width-boundary executions establish nonvacuity. Pinned source: anthropics/formal-math@16a5ce4, 3sum-apsp/ThreeSumApsp/Programs/Sec2/Theorem5/Encode/AllBands.lean:230-239,262-271 and BandArrayFacts.lean:107-113. Verified checkout files equal their pinned Git blobs and all PR-draft quotations match those exact line slices. The source's row/column encoding predicates map to runs' quantified original matrices, all bands and all leaves on computed MaskTable.layout; Light limits/program maps, callee contracts and source time hypotheses are replaced by actual native code proofs, not imported. The block index is beta*K0+(side? h:g), and row is block*N0 plus the compressed outer offset. Shared tile pointers and retained table words are exposed by tileInputBases/tile_input_values/table_word_layout. Reuse unchanged WordRAM control/rename/copy/signed APIs, Layout/bandArray/encoding mathematics and Mathlib finite index/sorted-set APIs. New mask scans, dense inverse lookup, direct base-seven decoder and native execution/cost composition are original. Small native-power/ordered-filter/positional-digit/row-major lemmas live in narrow topic modules. Retain Anthropic, PBC source credit and NOTICE. Validation: PASS all six strict gates (build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style, checkInitImports), serial Smoke/Axioms warmups and the global Axioms audit; full citation-aware hygiene --check-simp, fresh actual-base changed-file lints, strict PR-name and diff checks. Validated with LEAN_NUM_THREADS=1 and cache downloads disabled. Windows static metadata reads used PYTHONUTF8=1; no Lean/source change was needed. New Lean files use ordinary non-executable file modes. Exact payload tree bdfc5a1. Targeted Lean MCP endpoint/tests and pinned quote identity also pass. No PR has been opened; independent exact-revision correctness/API/source-mapping review is pending. Abstract assessment: no impact on selected abstracts, models or scope; no new headline or PDFs. Pruned queries, products, solvers and whole ordinary 3SUM remain open under #1394. Base #1520 remains unchanged at 3b9234d. AI assistance: Codex implementation/proofs, session codex-native-bandprep-t3-03b600bd, under delegating-worker coordination. Existing unchanged encoder outside-review evidence is PR1520#issuecomment-6477077023; final new-component review pending.
…tions Work in progress for #1526, not a submitted component. Complete native parent accumulation loop (31N+3), internal sparse initialization (7N+8), computed child push (15), shared actual frame-word store, executable query-code inverse/requested-set bridge and recursive timestamp allowance. These current modules have clean targeted Lean MCP diagnostics; actual interpreter and kernel digit/request regressions pass. Changed-scope hygiene --check-simp and diff check pass. The general node/controller continuation proof, actual initialized full evaluator theorem and final sparse charged bound remain unfinished; no full six-gate or independent review claim. AI-assisted implementation by codex-three-sum-continuation-t3-3dda8289; full #1394 remains open. Final current-tree checkpoint: strict build --wfail --iofail of Accumulate, Clear, Push, Frame, Powers, Leaf, Weight, Scan and SchonhagePruned tests passed together (3596 jobs); scope hygiene --check-simp and diff checks pass. This is a partial implementation checkpoint, not an all-six-validated PR or completed #1526 milestone.
WIP #1526. Factor root scan setup and root finish; prove the actual eleven-instruction root-frame initialization and exact memory/register frame. Current Root MCP diagnostics clean. Full node/controller composition remains unfinished; no PR or full-six claim. AI-assisted continuation by codex-three-sum-continuation-t3-3dda8289.
Address the sole P2 finding from the independent #1523 review of cb261f6: remove duplicate Nat.ofDigits_ofFn and publicly import the existing radix module. The finite-function numbering bridge uses Nat.ofDigits_ofFn_eq_sum. Its statement is unchanged. Existing radix declarations, proofs and source credit are unchanged; no native program, endpoint statement or test changed. Validation on exact final tree 4807cb9: PASS all six strict gates together (build --wfail --iofail, mk_all --check, test --wfail --iofail including global Axioms, lint, lint-style, checkInitImports), fresh actual-base changed-module lints (29 library/1 test), full citation-aware hygiene --check-simp, strict draft-name and diff checks. Serial LEAN_NUM_THREADS=1; optional cache downloads disabled. Lean MCP also reports clean diagnostics for the changed bridge. Logs are in .lake/codex-three-sum-continuation/band-review-six in the continuation checkout. Original native implementation and all full correctness/API/source-mapping review coverage retained. Review record: #1523 (comment) Original implementation/validation handoff: #1523 (comment) Focused final delta review pending before PR publication. No impact on selected abstracts, models or scope; no new headline. Complete #1394 native 1.9992 endpoint remains open. AI assistance: bounded reuse fix and validation by Codex session codex-three-sum-continuation-t3-3dda8289. Original author credit remains on cb261f6.
Continue #1526 implementation under #1394; this is explicitly partial WIP, not a complete component or PR submission. Full recursive node composition, initialized input/flat clients, derived global fits and total-time theorem remain open. No solver or all-state fit/execution/time certificate is assumed. Check full root setup/scan/frame (20Q+19), report (9Q+3), leaf/return (24), loaded leaf step (43), internal entry (7N+28), native nonempty child scan/push (20N+42), empty-child scan/advance (20N+33), returned-child accumulation (31N+29), and final return (26) against the actual standard fixed native Code. KernelRegs describes only constant/pointer register values. Node footprints preserve the ancestor rows. The zero-depth node matches existing Pruned.result and the finite traceWeight; its continuation uses the existing ExecWithin.loop_iter. No alternative machine or run semantics is introduced. The reporting-body/controller names are definitionally identical Code trees. ScanMemory.congr transports the existing representation across disjoint writes and removes duplicate root proof plumbing; push exposes its four-store frame. Validation: targeted Lean MCP diagnostics clean for every new/updated phase and ComplexityTests/SchonhagePruned.lean. Native interpreter regressions retain depths 0/1/2, both signs, repeated/empty/mixed queries and an outside sentinel. New kernel examples discharge the general node/register/address/signed premises, connect the same negative-product final memory to charged controller execution, and prove an empty leaf preserves the prior value cell. Diff whitespace passes. No aggregate/all-six validation claimed: root/native audit coordination hold is respected. Exact partial checkpoint tree 7fa4da6. Abstracts: no impact; no new headline or endpoint claim. Original 1.9992 objective and sparse-product/ET/final composition remain open under #1394. AI assistance: Codex implementation/proofs by continuation worker codex-three-sum-continuation-t3-3dda8289.
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.
Finish bounded #1545 from exact #1536 head66036150a. Replace generic level/inner/outer API vocabulary with order-embedding/subset/complement names. Remove five redundant membership/range/congruence wrappers, using Mathlib's orderEmbOfFin_mem/range_orderEmbOfFin and ordinary substitution directly. Migrate every actual Levels/Batch proof client with no deprecated aliases. Keep filter_glue's generic name and rename its predicate parameter to P. The retained generic statement headers are identical after the documented renaming and binder alpha-renaming. All 48 Levels and 13 Batch declaration statements and all definition bodies remain unchanged. The entire native Encoding module is token-identical after comment removal; every other native library file is unchanged. Source credit and pin are retained. Thus existing State.init, Signed.encode, width/frame/cost and encodingL/R meanings remain. Put the sum/option-versus-flat-digit explanation at the actual leftDigits, rightDigits and termDigits hover docs, preserving their enumeration bodies and order (row-major P terms, P0 digit9). Update the UPSTREAM naming follow-up. Add generic nonconsecutive signed/zero/Option reconstruction clients using Mathlib's orderEmbOfFin_unique, plus the routed optional #1536 asymmetric native L4,m1,N29 prefix tests. Those compute headers/count/tables/snapshot and decode/read ranks1 and2 with K0=2, distinguishing quotient/remainder blocks and signed values without a full10^4-leaf encoder run or native body edits. Reuse unchanged outside coverage: PR1496#issuecomment-6477111644 atb4936ce28, PR1496#issuecomment-6480746578 at68bbe40e3, and PR1536#issuecomment-6480852097 at66036150a12046b29986d8f108c0afaf49d01c61. These are agent reviews, not human approval. No new cited mathematical result or machine model is introduced. Validation: PASS build --wfail --iofail, mk_all --check, test --wfail --iofail, lint, lint-style and checkInitImports, with serial Smoke/global Axioms warmups. Full citation-aware hygiene --check-simp, fresh changed-file lints against actual base66036150a, strict PR-name and diff checks, and source/native identity checks PASS. One thread, no cache downloads, PYTHONUTF8=1 on Windows. Targeted MCP checks, full hygiene --check-simp and source/native identity checks pass. Final source tree: 0c21b60. No source/ancestor merges or restacks. Abstract assessment: no impact; no selected theorem/model/meaning/scope or PDF change. This is generic ergonomics/testing only; full #1394 remains open. AI-assisted implementation by codex-native-bandprep-t3-03b600bd, under parent continuation-worker coordination. No new review agent commissioned; ordinary outside coordinator review is requested when the bounded PR is ready.
WIP checkpoint for #1526; no PR and no completed component claim. The actual fixed native controller now has a depth-inductive execution proof with original Pruned.result values, stored queries/frames, concrete spatial preservation, input-derived signed fits and traceWeight charged continuation. Root loop exit discharges the continuation. All new library modules through Recursive.exec_ready have clean targeted Lean MCP diagnostics. New concrete entry/result client reports no diagnostics, but the complete existing test file is still elaborating its VM regression commands; no final test-pass or all-six claim. Initialization/root-list/report/flat State.init composition, global width/fit clients, full component validation and independent review remain open. Aggregate checks are held for the coordinated root validation slot. GenericRAM/Signed/Fits.lean is the unchanged blob from independently owned PR #1552, commit f276db1; credit retained. No native program body changed in this checkpoint. All proofs and invariant definitions are original native work; existing mathematical pruning/encodings retain their source credit. No selected-abstract impact or whole-3SUM endpoint claim. AI-assisted implementation by codex-three-sum-continuation-t3-3dda8289.
…selection Complete #2098 source on exact counter PR prerequisite4027bd980. The actual 160-register standard program enumerates the existing prime square window with native trial division, invokes the entire native cyclic-Strassen counter on original canonical signed matrices, and returns an attained minimum. Original arguments, dirty workspace and outside-source frames are derived; there is no supplied counter/run/time/prime-list/layout oracle. Generic caller plus actual15-instruction header yield original State.init prefix and charged halt in the same final state. Flat code<=32824 slots, no width reads. D>=16 suffices even for empty matrices or D>n. For D<=n, kappa>=1 and original weights<=(n+2)^kappa, positive sufficient physical width (kappa+30)*clog2(n+2) admits every wider execution; all successful prefix words/support are below (n+2)^(2*kappa+60), independent of physical W. Complete charge including header/halt <=3704*(sqrt(D)+1)^3*(n+1)^2.81 +42*(D+1); D dependence remains explicit. Existing IsSelectedPrime directly supplies the finite false-positive bound. Native tests prove actual update, stable ties and empty behavior; admitted clients connect actual State.init to selected prime3, exact count0, frame and the real source-regime FP theorem. Reuse the counter private numerical-admission proof by exporting it as CountPrime.admission_fits in its existing Width topic module and migrate its one internal client. Old counter public statements/programs remain unchanged. New modulus-budget monotonicity lives beside the actual counter/Strassen budgets. Abstract/catalogue/rendering unchanged. Source adaptation checked against Anthropic pin16a5ce41304fcdaea4e0be7c132e1c361dc26da5 ChoosePrime bytes17572 SHA256e9e7e9b8f8947d36043d8b1b8445a29d2ce90a004b2b88d8714f8701c1ec7280. chKeep/chRound95-107 policy reused; trial enumeration replaces the source prime-list producer109-118 and all native costs are independently proved. Validation at source checkpoint: targeted MCP checks clean through complete caller/header/input/width/flat/source/time composition and full initialized native test module, including actual kernel/VM clients. Canonical imports generated and check passes; hygiene--check-simp and full diffs clean. Source proof errors during development were fixed before these final diagnostics. Fresh whole-layer nonauthoring review, final scoped/static audit and exact-head hosted six-gate CI remain required. No local full-six claim. Global parameter/small-geometry/outer ET/ordinary-host composition and full #1394 exponent1.9992 remain OPEN. AI assistance: OpenAI Codex.
Implement #2127 as a child of reviewed selector1c290ca70. New original coarse family t=floor(log2(n)/1296), m=36t, D=4^m, g=4^t, L=19m. Prove g^36=D, D^18<=n for positive n, n<(4g)^648 and exact fast threshold t>0 iff2^1296<=n, which supplies D>=16. Small/zero inputs are classified, not assumed to satisfy fast geometry. These are not Anthropic tuned parameters or the final exponent1.9992 theorem. Actual fixed16-bank standard code reuses native NatLog and two Power calls; all logarithm/division/multiplication/power/copy/branch/header/halt instructions are charged <=12*log2(n)+36. At most128 flat slots inclhalt, no width reads. Generic caller uses original raw n and one derived word envelope; all memory and n are preserved. Original State.init[n], prefix, halt and all parameter outputs use one final y. Positive sufficient width <=12*clog2(n+2), every wider prefix words/support <(n+2)^13 independentW. New Power/Rename topic exposes the existing concrete execution in an injective bank with full input/memory/outside-bank frame, reused twice. Source/API paths: pure ParameterChoice and native DyadicParameters are new. All existing library/test files, especially the original15-register native Parameters splitting API, remain byte/mode-identical to parent. Only new modules, canonical imports and scoped coordination docs are included. No abstract/catalogue/rendering impact. Validation at this source checkpoint: Lean MCP clean for all new math and complete native initialized/kernel/VM suite, plus original chunk client. Actual VM boundary below/at2^1296, zero and dirty caller sentinel; fully admitted same-y original-input/kernel geometry and wider-prefix clients. One test-only exponentiation threshold permits this concrete1296-bit numeral; no heartbeat/recursion/axiom/sorry override. Canonical imports check and full hygiene--check-simp/diffs pass. Scoped strict/static checks and fresh nonauthoring review are next; hosted exact-head six-gate CI required before integration, no full-local-six claim. Callable fixed-prime solver #2125 proceeds independently; selected-prime composition, aggregate asymptotics, small-case solver dispatch, outerhost and full #1394/1.9992 remain OPEN. AI assistance: OpenAI Codex.
Source/MCP checkpoint for #2125 on pinned bc2. Complete actual640-register caller execution, original-array copy/sum, computed source width and memory-window translation, exact +/- ET/witness/global scans and caller/selector frames are proved. Aggregate actual source/copy/setup/return/halt charge and original initialization14 are checked. All owned source modules and concrete signed/dirty/frame/cost tests have clean targeted diagnostics; no local all-six/static/import audit claim. Original producer admission/locality proof is reused through narrow public seams; old initialized statement and all existing native source program bodies are retained. This is a partial source checkpoint, not completion/publication: full initialized same-y Runs/halt, original-regime logarithmic width/polynomial prefixes, fully admitted clients and final audit/review remain under2125. Root retains sole audit slot and full1394/global parameter/prime/ordinary-host/asymptotic scope. No new agents or PR. AI assistance: OpenAI Codex; original source credit preserved.
Source-ready checkpoint for #2125 on pinned main bc2e6c2. Complete fixed640 standard Code caller and initialized entry: real original-array copies/sum, native ceiling-log/power/modulus/normalization, actual complete one-time producer and all-record solver, original signed witness verification, raw Boolean/witness/global scans. Caller preserves low160 and arguments600..607, with outside-window/source frame and dirty scratch. Actual initialized same-y prefix and halt prove positive and negative ET iff, and global S<=F(p)+actualFlag. No run/layout/list/witness/solver/time oracle. New Width/Prefix/SourceBounds prove original-parameter positive admission, raw dirty words before reduction, every-wide-width native prefixes and independent-W polynomial words/new-support. Separate caller placement/raw-word exponent is explicit. Initialized log-width coefficient24664*(kappa+9)+19 and polynomial prefix exponent24664*(kappa+9)+20. Actual caller cost24n^2+24669*clog2(n+D+g+p+T+4)+482+3*oldSourceTime pre-halt, T actual raw copied sum. Initialized header14 and halt1 are charged. Complete source aggregate terms retained, including one global false-positive reserve; parameter/prime choice, uniform selected-prime performance and full1394/1.9992 remain OPEN. Targeted Lean MCP clean: new umbrella and all source through its imports; three owned test modules WordRAMCallableFixedPrime, WordRAMCallableFixedPrimeInput, WordRAMCallableFixedPrimeCaller; existing WordRAMExactTriangleFixedPrimeInput client. Tests include fully admitted initialized +/- valid thin geometry, complete actual dirty caller with aliased inputs/nonzero low160, and small native signed/header/return/frame/cost regressions. Earlier source files checked serially; bootstrap was warm. No local all-six, canonical aggregate generation or final hygiene/name/static audit claimed: root retains that slot, required fresh whole-layer review/publication still pending. Original source checkpoint37de retained. Own new-file executable modes corrected to0644; no unrelated checkout/cache/process/source change. Public producer exec_at/input_fits and Output transfer/heap lemmas reuse original private admission/locality proofs; old initialized statements and existing native program bodies retained. FixedPrime noReads property extracted once and reused. Generic ArrayCopySum/MemoryWindow normalization API additions have concrete clients. Abstract catalogue/rendering unaffected; no headline promotion. AI assistance: OpenAI Codex; existing mathematical/source credit retained.
Only mode100755 to100644; source bytes and targeted Lean evidence from69495f23b unchanged. Source-ready2125 still awaits coordinated canonical imports/static and fresh whole-layer review; no all-six claim.
…ee-sum-native-callable-fixed-prime-20261101
…tion Final #2125 candidate on one normal compatibility merge of pinned main b4678e2. All28 source-ready owned source blobs and modes are identical to61fec4343, all inherited main blobs preserved, and only22 canonical imports added. No source/proof/program repair during this final audit. Frozen validated source tree ff0dd30. Strict cache-disabled scoped build PASS for new CallableFixedPrime umbrella, all3 owned tests (WordRAMCallableFixedPrime, WordRAMCallableFixedPrimeInput, WordRAMCallableFixedPrimeCaller) and existing WordRAMExactTriangleFixedPrimeInput. Canonical mk_all check PASS; full hygiene --check-simp PASS; changed25-library environment lint PASS (538 local declarations, imported-environment nonlocal linters too); fresh scoped compiled doc-name/3-new-test audits PASS; strict PR body declaration names PASS; whole pinned-base/staged/unstaged diff --check PASS. One compiler thread, downloads disabled. Exact own/supplier/main/native-code/statement/private-fit and primary-pin/blob/locator identities PASS. All audit processes finished. Scope limitation: NO local whole-library/all-six claim. Standard changed-file CLI first rejected missing whole-library freshness/root artifacts, including unrelated WordRAMUniformProbing. Its unchanged repository doc/test lint functions passed on fresh strictly built scoped25lib/3test artifacts instead; full standard CLI and all six gates require hosted exact-head CI before integration. Initial mk_all generation exit1 denoted one updated aggregate; subsequent check0. Initial lake lint argument parsing fixed by direct existing Batteries script; no source workaround. Preserved raw logs/summary/validation and reproducible audit helpers under tmp/callable-fixed-prime-3dda8289/final. Code/model: fixed640 standard caller protects low160 and args600..607, returns raw632 flag/633..635 original witness/636 global scans; actual signed copying+sum/native modulus/dirty normalization/one producer/all-record execution, initialized same-y prefix+halt, exact positive AND negative ET iff, global S<=F(p)+actualFlag and caller frame. Original D4^m>=16, n>=D^18,g>=1,p-window and raw old-word/address bounds explicit. Complete charged preparation/product/query/control/scan/compiler/copy/setup/return/halt bounds, positive source-regime log admission and independent-W polynomial prefix/support proved. Full parameter/prime/outer host/asymptotic1394/1.9992 remains OPEN; no selected-prime/uniform fast endpoint claimed. Fresh whole-layer nonauthoring review remains REQUIRED before publication, covering CopySum, normalization, producer exec_at/input_fits/locality, dirty source derivation, actual640 caller/init, every-wide prefix and costs. Unchanged supplier reviews are not approval of new reasoning. No PR/watch/merge by child. Abstract/catalogue/rendering no impact. AI assistance: OpenAI Codex; existing source credit retained. Canonical imports are the only source delta from the source-ready checkpoint plus pinned-main compatibility.
Implements milestone #2145 on exact #2133 f92e5c6, ordinary work/three-sum-native-et-aggregate-cost-20261101. Original conservative arithmetic on actual proved parameter/selector/fixed-prime charged functions: exact roots/powers, rounded query capacity, one global selected-prime scan reserve, selector absorption and explicit cubic-over-groups saving. Fast regime is n>=2^1296; original weights bounded by n^kappa, kappa>=1, actual existing selected-prime predicate retained. No supplied execution/solver/layout/time contract. n^3/g<=4*n^(3-1/648); logarithmic factors still explicit. This is not a composed program or tuned1.9992 endpoint. Strict scoped build PASS for DyadicCost, new WordRAMExactTriangleDyadicCost and inherited native parameter test; all new source/clients targeted checked. Scoped environment lint PASS; canonical mk_all check PASS; full hygiene --check-simp PASS; unchanged compiled doc/test checker APIs PASS on fresh two-library/one-test outputs; strict body names and full-base whitespace PASS. Parent library/test/abstract blobs unchanged; new source LF and modes0644. No local full-six claim; hosted exact-head CI must supply six gates plus the full standard artifact check. Scoped checker records4433 missing unrelated ileans explicitly, not a whole-library pass. Initial own RecordProduct.Flat cached read-only artifacts fixed only after nlink1/own-path verification; setup retry succeeds. Logs retained under tmp/et-aggregate-cost-20261101. Infinite dyadic-family client discharges actual fast geometry and original zero-matrix weight premises, obtains a selected prime, applies all component budgets and checks real-power saving. It is a kernel cost client, not an enormous interpreter experiment. Fresh independent whole-layer API/correctness review required before publication. No abstract/catalogue/rendering impact or claimed Anthropic tuned constants; existing hashing/scanning/native suppliers reused. Root1394 full ordinary-input/native-host/width/asymptotic composition remains open, with actual solver assembly separately owned under2146. AI assistance: OpenAI Codex.
Follow-up under #1394 on reviewed #2147 exact4e48de9e2 (all six hosted gates passed). One new original arithmetic module and one test; inherited native/math/API source unchanged. Reuses Mathlib isLittleO_log_rpow_atTop and Real.natLog_le_logb. For each real kappa>=1 one thresholdN>=2^1296 bounds every actual native parameter/selector/selected-fixedprime component allowance by4*n^(3-1/1296), uniformly over original three matrices bounded byn^kappa, selected prime, reference memory and physical width. Threshold is chosen before those data. Native component functions have no width argument. No time/run/layout/solver contract, no new executable code or effective threshold passed as algorithm input. Public theorem retains existing native budget's positivity proof explicitly, which also follows fromN. Original constants/tuned1.9992 not attributed or claimed. Main/new closed zero/+1/-1 constant-input clients pass targeted Lean MCP. Strict scoped build new Asymptotics module/new SubcubicBudget test/inherited DyadicCost test PASS19.99s; scoped environment lint PASS27.24s; canonical mk_all check/full hygiene --check-simp/scoped compiled doc+newtest APIs/strict body names/base whitespace PASS. Old source/abstracts unchanged, own LF/mode0644. Scoped checker records4433 unrelated missing ileans; hosted exact-head CI must supply full six gates and the standard full artifact check. No local all-six claim. Evidence under tmp/et-subcubic-budget-20261101. Fresh independent source/API review required before publication. One local library proof and one test permit1296-bit fast-threshold numeral normalization; no heartbeat/recursion override. Asymptotics proof absorbs all logarithms into half the previously proved1/648 saving. It proves component cost arithmetic only: #2146 actual solver/small-case assembly, callable adaptations/control, final ordinary-host/width/asymptotic composition and #1394 exact1.9992 remain OPEN. No curated abstract/catalogue/rendering impact. AI assistance: OpenAI Codex proofs/tests; existing supplier/source credit retained.
SOURCE CHECKPOINT for #1394/#2146, not a PR/final-validation candidate. New CallableFixedPrime.dyadicTime(n,F) and timeBound_le_dyadicTime have clean targeted Lean MCP diagnostics. The natural mathematical time function uniformly bounds actual fast initialized ledger Param.timeBound n+Selector.timeBound n(window n)+CFP.timeBound+42, for every proper original array bounded byF, selected prime and reference memory. It depends only on original n,F; no content/layout/run/time certificate. The underlying program does not compute the real ceiling time metadata. Uses actual source/copy/modulus costs and pointwise auxiliary weight exponent1+log_n(F+1) in the existing finite selected-prime theorem. Sixteen extra reserve includes assembled initialized header/halt and also covers the generic caller+26. Runtime budget definitions and all supplier native code are unchanged. Existing private coefficient proof from #2148 is exposed as costCoefficient/costCoefficient_eventually_le_rpow for the concrete new cost consumer, removing the old private name without compatibility wrappers. Old public uniform threshold statement is unchanged; module targeted diagnostics clean. Normal prerequisite merge of exact reviewed #2139 dc927 into #2148 97fbc0f; inherited main source is retained unchanged. NO imports generation/static/full-six/final independent review claimed for this checkpoint. Root still proving uniform polynomial-F asymptotics and actual initialized selected-prime corollary on this branch; one new untracked in-progress execution file is not part of this commit. Root holds sole audit slot. #2146 may merge THIS pinned API checkpoint to finish actual Callee; published supplier branches unchanged. Full1394/1.9992 remains open. AI assistance: OpenAI Codex.
… time Complete #1394 milestone: natural dyadicTime depends only on original n and F; pointwise actual parameter/selector/callable ledger +42 is bounded for every selected prime and arbitrary reference memory. Uniform C,N are chosen per natural kappa>=1 before F<=(n+2)^kappa, contents, selected p or width; the natural function is O(n^(3-1/1296)). Actual initialized callable prefix and charged halt preserve one final state with exact signed verdict, original witness and input frame at the derived logarithmic width. Selected p is still supplied to this subroutine; parameter/prime dispatch remains #2146. No clock, layout, run or time law is an input oracle. Full #1394/1.9992 remains open. All final source MCP diagnostics clean. Strict scoped compilation passes new Cost/Execution/test, parent subcubic-budget test and old initialized callable client. Canonical mk_all check, environment lint over 3 libraries+test, full hygiene --check-simp, fresh scoped compiled doc/new-test checker APIs, strict PR names and whole-base whitespace pass. Standard whole-library artifact validation is unavailable locally (4491 unrelated ileans absent); hosted exact-head all-six plus standard checker validation required. No local full six claim. No machine program or curated abstract changed. Independent nonauthoring /root/natural_runtime_review APPROVE whole layer; /root/natural_runtime_api_delta_review APPROVE exact subsequent coefficient monotonicity move, verifying inverse transforms recover whole reviewed source. Review source hashes match final files. Agent review, not human approval. Normal combined prerequisite 22f07e4 carries unchanged #2139 dc927 plus #2148 97fbc0. Of 4903 inherited Lean/abstract paths, only the declared existing DyadicCost.Asymptotics coefficient API extraction is changed. New own Cost, Execution and test files plus 2 canonical imports complete this layer. Original composition of existing proved costs, no new external quotation or endpoint claim. AI-assisted by OpenAI Codex. Local reproducible packet: tmp/callable-et-cost-20261101/{validation-summary,source-identity,changed-file-check}.json and final-{strict-scoped,environment-lint,hygiene,pr-names}.log; public PR owns final validation and review. Detailed source mappings in module/PR text.
Collaborator
Author
|
Independent nonauthoring agent review of the whole new mathematical/API layer at c7b9fcf: APPROVE, by The full review checked the auxiliary weight exponent, arbitrary-memory/selected-prime pointwise bound, actual wrapper/header/halt charges, threshold ordering before all polynomial F and input data, ceiling estimate, exponent 3−1/1296, and the actual same-y initialized prefix/halt, input fit, original verdict/witness and frame. The 0/1/−1 constant-input clients discharge all premises and return literal answers. The reviewers confirmed the supplied-selected-prime restriction and that no assembled selector, small-case solver, 3SUM endpoint or source-trace equivalence is claimed. The one optional API finding was fixed: coefficient monotonicity now lives beside |
This was referenced Nov 1, 2026
SamuelSchlesinger
approved these changes
Nov 1, 2026
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
Collaborator
There was a problem hiding this comment.
Non-author coordinator agent review by codex-native-dyadic2154-20261101 of c7b9fcffc840dd2bf3f60a71883f67f189935906: APPROVE. I reuse the existing full/API coverage, checked the actual five-file new layer and its execution interfaces, and verified source identity before reusing prerequisites: all 28 callable-solver payloads match #2139 at dc92727dc, and 49 parameter/counter/component-cost payloads match #2148 at 97fbc0f9.
The quantifier order is correct: one positive coefficient and finite threshold per natural κ≥1 precede n, F, values, selected p and every sufficiently wide W. The fixed program does not depend on these proof constants. The auxiliary weight exponent, coefficient monotonicity/log absorption and ceiling estimate give the stated exponent 3−1/1296 uniformly for F≤(n+2)^κ. The new execution theorem uses the real initialized run, derives input admission and fast geometry, charges header/copies/setup/control and the final halt, and retains the same y for bounded state, original verdict/witness and input-prefix frame. The 0/1/−1 clients obtain selected primes and literal accepting/rejecting executions with every premise discharged.
The scope remains conditional native WordRAM instruction cost. The initial input already contains the computed geometry and a selected prime; this subroutine does not execute their selection, though its allowance conservatively includes those charges. The noncomputable ceiling is descriptive metadata. Initial input construction, ordinary bit-cost/host composition, the small-input branch, broader Schönhage/3SUM claims and the tuned 1.9992 endpoint are not established here. Source credit and the own layer’s no-impact abstract assessment are correct.
I verified that hosted CI passed all six gates and changed-file checks; no duplicate local build. #2148 and the explicit #2139 supplier remain open prerequisites, so this is source approval, not a claim that the current stack is ready to merge unchanged. Agent review, not human approval.
Collaborator
|
Prepared — bounded worker The own layer is exactly the five-path delta after joint-parent merge No new proof/API repair, mathematics review, Lean build, log retrieval, original-branch push, retarget, queue or cache action. Original implementation ownership, credit and review 5729897050 remain unchanged. The supplied-prime/component/asymptotic scope and full #1394 gap remain explicit. Fresh canonical validation is still required after audited publication. |
Merge fixed actual main851fa3f5, containing actual #2139/6daf and #2148/851, into approved sourcec7b9fcf. The true own layer starts after joint parent22f07e41=[2148/97fbc0f,2139/dc92727d], not at the PR display base; inherited sibling code is not new feature work. Preserve all four reviewed code/test payloads and their documentation. Replay the complete original five-path feature, including imports, forward and backward exactly. Resolve only generated imports, exact reviewed Asymptotics bytes under main==joint-parent guard, and the unchanged-child ROADMAP conflict by retaining exact actual main. All5328 unrelated main entries/pins remain exact; imports are canonical3899. All28 callable payloads and107 parameter-branch code entries have explicit parent guards; the sole shared Asymptotics change is the already reviewed own-layer API/proof move. Validation is source-only preservation and own-delta whitespace. No Lean/build/CI-log download or full-six claim. The old-source-relative whitespace note is inherited exact-main scripts/test_guide_selection.py:149; no unrelated cleanup is introduced. Root independently audits this unpublished checkpoint before publication; fresh canonical CI follows. Original Edemaine/t3 implementation credit and outside review5729897050 are preserved. Supplied-selected-prime/component/asymptotic scope and full #1394 gap are unchanged; selected abstracts have no impact. AI-assisted integration preparation: OpenAI Codex (codex-prep2154-1730-20261102), delegated by LogsQ. No new mathematics, approval, source-branch push, retarget or queue/cache action.
SamuelSchlesinger
changed the base branch from
work/three-sum-native-et-subcubic-budget-20261101
to
main
November 2, 2026 04:42
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
Collaborator
There was a problem hiding this comment.
APPROVE the source-preserving main refresh — coordinator codex-root-2205-20261101, at b31a3939480a0be5084b01528e6a64f8de333048, reusing the outside source/API review.
The four reviewed code/test entries and their complete patch are unchanged. I independently applied and reversed the entire original five-path feature, including the aggregate, recovering the exact candidate and landed main without fuzz. The shared Asymptotics override matches its reviewed parent before replay; all 5,328 unrelated main entries, pins, source credit and catalogue scope are preserved. No new proof, public meaning or mathematical review count.
Fresh required CI and current-prefix validation remain before integration. This is agent review of preservation; the supplied-prime/component scope and broader #1394 gap remain unchanged.
Collaborator
|
LogsQ coordinator: #2154 is complete through usable publication. Actual The first actually started containing main consumer was fixed before retrieval at that same This is the initialized native allowance for supplied computed geometry and a selected prime. Selector/solver assembly, small-case dispatch, bit-cost interpretation and full #1394 remain separate. The #2205 C2 chain keeps priority; its next #2246 source is now published for fresh validation. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Advances #1394 with a natural runtime function that the actual ET callee can use. Stacked on #2148; unchanged #2139 is an explicit sibling prerequisite, including its normally merged main snapshot. This adds mathematical composition and checked execution clients; it does not add machine instructions or finish 3SUM.
CallableFixedPrime.timeBound_le_dyadicTimebounds the actual parameter, selector and callable ledger, plus 42 instructions, bydyadicTime n Ffor every fast dimension, original signed input bounded by F, selected prime and reference memory. The natural allowance depends only on n and F. Its ceiling is descriptive mathematical metadata; the program neither computes it nor receives it as a certificate. The proof uses an auxiliary exponent 1+log_n(F+1), the existing selected-prime/component estimates, and the real wrapper charges.CallableFixedPrime.exists_dyadicTime_subcubic_boundchooses one positive C and threshold N per natural κ≥1, before every F≤(n+2)^κ, and bounds the natural allowance by Cn^(3−1/1296).CallableFixedPrime.exists_dyadic_runs_thresholdconnects this allowance to the existing program's actual initialized prefix and charged halt, at every W≥(24664(κ+9)+19)*clog₂(n+2), with input fit, exact original verdict/witness and preserved input prefix in the same final state. Runtime p is still supplied and assumed selected; this theorem does not execute prime selection. The allowance conservatively includes its cost. Parameter/prime dispatch and the genuine small-input branch are assembled separately under #2146.The coefficient, its monotonicity and its eventual logarithm absorption are exported from the existing topic module for this concrete client; the previous component-threshold theorem remains unchanged. New clients discharge every premise for original constant matrices with weights 0, 1 and −1, obtaining actual selected primes and actual same-state executions. These are Lean kernel clients, not gigantic interpreter fixtures. This is original conservative composition of existing proved native bounds, not a claim of Anthropic's tuned constants or the 1.9992 endpoint. No new source quotation, execution model, axiom or supplied run/time law is introduced.
Validation: strict scoped compilation passes for the complete new layer, its execution test, the parent budget test and the existing initialized callable test. Canonical imports, scoped environment lint, full hygiene/simp, compiled doc/new-test checker APIs and strict name/whitespace/identity checks pass. The checker APIs used fresh scoped artifacts; unrelated whole-library artifacts are absent locally. The hosted exact-head run passed all six Lean gates and the standard changed-file check on c7b9fcf; no local full-six claim. Unchanged #2139 suppliers retain their existing independent review and hosted validation.
Independent nonauthoring agent
/root/natural_runtime_reviewapproved the complete mathematical/API layer;/root/natural_runtime_api_delta_reviewapproved the subsequent exact proof move exporting coefficient monotonicity. Reviewed source digests match the final candidate; both ran source review only. Their consolidated review record records the checked reasoning and resolved API finding. This is agent review, not human or platform approval.Full #1394/1.9992, the ordinary host composition and the tuned parameter analysis remain open. No curated abstract/catalogue/rendering impact: this remains a conditional selected-prime ET milestone. AI assistance: OpenAI Codex authored the proofs/tests and a separate nonauthoring agent reviewed the new layer; no human approval implied.