Repository navigation
feat(ExactTriangle): assemble a parameter-selecting native solver - #2155
Merged
karnseth merged 183 commits intoNov 3, 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.
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/MCP checkpoint for #2146, continuing 42638e9 without parent or toolchain changes. The actual fixed640-register code now has general original-caller execution, both exact original ET verdict directions, computed parameter/small dispatch, real minimum-count prime selection and full fixed-prime solving, original argument restoration and caller/outside frame. The derived prime/reference memory index the actual charged ledger; neither is an algorithm argument. Fast pre-halt cost is actual parameter time +actual selector time +unchanged CFP.timeBound +26; slow is actual parameter time +39n^3+33. The initialized header and halt add16. No supplied execution/selection/layout/time/solver certificate. Actual CountPrime.inputWords(n,F,values) initialization is proved: the second raw header means original F, all three signed matrices follow, original pointers3/3+n^2/3+2n^2 and free3+3n^2 are computed by15 instructions. The same y witnesses prefix Runs, charged halt, bool/ET iff, selected-prime-or-small tag, frame and restored six arguments. Actual initialized program <=434015 slots including halt and noReadsWidth. Every admitted wider caller and initialized prefix has a numerical word/new-support bound independent of W, supplied by the real minimum-width complete execution. General semantic exec_at has NO old-word/P premise and does NOT claim arbitrary unused old words are W-bounded. Resource caller admission separately includes original raw P before dirty loads. Polynomial original weights/placement/P imply logarithmic admission and independent-W polynomial prefixes; initialized all-n coefficient is 12332*(kappa+9)+40 and word/support exponent12332*(kappa+9)+41. Host semantic admission123357*clog2(free+F+n+2) needs no old-word/P assumption. MatrixInput.exec_matrices derives row-major proof-only serialization/readback from original matrix functions; no native copy/table oracle is inserted. Targeted Lean MCP diagnostics clean for all new execution/input/prefix/source-bound/matrix-client modules, plus three test modules (small actual VM regressions already in42638, new complete initialized and arbitrary dirty alias clients). Fully admitted initialized n0/F0 negative prefix+halt<=82; n1 signed[-1,-1,2] positive<=121 and[-1,-1,1] negative; symbolic all n>=2^1296 and arbitrary signed z constant matrices return true iffz=0 with actual selected prime; complete alias caller permits unrestricted unused K/sentinel. Only the symbolic threshold client raises exponentiation.threshold to1300 for the exact fixed2^1296 constant; no heartbeat/recursion override. No all-six/global/static/import audit claimed or started: root retains sole slot. Earlier own isolated dependency repair and minimal target logs remain in tmp/parameter-selecting-et-3dda8289 as recorded in42638. Remaining #2146: content/layout-independent concrete Host.Callee time(n,F) bridge using root's in-progress explicit natural dyadicTime bound, then final docs/import/scoped validation and fresh whole-layer review. Existing source API deltas in Slow.exec_at and CFP.exec_at require affected fresh review; supplier approvals do not cover them. No PR/review/watch/merge. Full #1394/1.9992, final ordinary host and root cost/asymptotic work remain OPEN. AI assistance: OpenAI Codex; original supplier/source credit preserved.
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.
…ee-sum-native-parameter-selecting-et-20261101
Source-complete targeted checkpoint for #2146. Normally merged only coordinator-authorized d8f759b into own child, retaining published supplier refs/source. The merge brought the mathematical cost prerequisites and changed no toolchain/manifests/policy. CFP.dyadicTime and its pointwise+42 theorem are reused unchanged. ParameterSelecting.callee : ThreeSum.Host.Callee633 is now the actual640-register solver, with fixed original0..6 ABI, widthCoefficient123357 and natural callerTime(n,F) independent of contents/layout/W. Fast callerTime is actual CFP.dyadicTime; small is actual parameter time+39n^3+49, conservatively including header/halt even for calls. timeBound_le_callerTime discharges the real ledger+16 using the selected prime actually returned by the code, no numeric/run/solver/time premise. General arbitrary-old-data host correctness does not add Data.Bounded/P. runs_input_uniform preserves actual State.init same-y Runs, charged halt, input fit, bounded final state, both original ET verdict directions, selected/small tag, full frame and restored six arguments, under only original length/magnitude and derived numerical admission. All own source modules/umbrella and three tests have clean targeted Lean MCP diagnostics. Explicitly rechecked affected existing WordRAMCallableFixedPrimeInput and ThreeSumCaller clients: clean. Tests include actual complete signed/negative/zero/alias/dirty VM regressions; fully admitted initialized empty/F0 halt<=82 and signed[-1,-1,2] positive halt<=121, negative[-1,-1,1]; generic valid-fast n>=2^1296 and arbitrary signed constant z with same-y run/halt budget and trueiffz=0; arbitrary unused K alias caller; actual Host.Callee.exec signed[-1,-1,2] with ordered spans and arbitrary K/sentinel. No assumed fast solver, precomputed layout or execution/cost certificate. Existing semantic exec_at and raw-P prefix/resource distinction documented; positive original-input log admission and independent-W polynomial prefix/support proofs retained. ROADMAP/UPSTREAM retain full1394/1.9992 gap, distinguish original conservative family, actual composed solver and remaining global/outer-host/tuned asymptotics. No curated abstract/catalogue statement changes. Primary source pin verified exactly16a5ce41304fcdaea4e0be7c132e1c361dc26da5; original composition does not quote or claim the source's full tuned result. Draft mapping/review entrypoints in tmp/parameter-selecting-et-3dda8289/pr-draft.md. New Callee, exec_at extraction, matrix serialization and width reasoning require ONE fresh exact-layer independent review. Final canonical imports/scoped/static/source/name checks remain queued behind root's sole slot. No local all-six/global/import/static audit or PR/reviewer/watch/approval/merge started by this worker. Hosted exact-head full six required before integration. Source-ready candidate only; #2146 awaits final validation/review/integration. Full #1394 remains OPEN. AI assistance: OpenAI Codex; supplier/source credit preserved.
… 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.
Final candidate for #2146 on pinned coordinator cost prerequisite d8f759b. Frozen final Git tree: 1aa2788. The complete actual640-register solver computes coarse dyadic parameters, actual minimum modular-count prime, complete callable fixed-prime solving, or the real exhaustive small branch. Original host0..5 are restored and raw6 decides the existing original-weight ET problem. ParameterSelecting.callee : Host.Callee633 has widthCoefficient123357 and explicit natural callerTime(n,F), independent of contents/layout/W and without an assumed execution/time/solver/numeric contract or old-word/P hypothesis. Existing CFP.dyadicTime supplies the proved pointwise fast allowance; its source/resource meanings and all actual native suppliers are unchanged. Initialized header/halt add16, tied to the same y and both verdict directions. Generic execution is distinct from physical prefix bounds, which separately state the original raw bound P. Original-input log-width and every-wide independent-W polynomial word/support bounds include zero/small inputs. Final source changes after4205: canonical aggregate generation (19 own modules plus1 inherited d8 CFP.DyadicCost module); umbrella Callee633 corrected to Callee 633 plus three prose spacing fixes. Comment-erased code/proof/statement tokens are identical to4205. No semantic/program/API or dependency/toolchain/policy changes during audit. 498 other inherited supplier files and30 Slow native definitions are exact-preserved. Old CFP.exec statement and Slow.callee statement/code/time/width fields are preserved; new CFP.exec_at extraction and Slow.exec_at generalized-span reasoning still require fresh whole-layer review. VALIDATION on the final tree: cache downloads disabled, two compiler threads. lake --no-cache build --wfail --iofail succeeded for ParameterSelecting umbrella, all3 new tests, existing WordRAMCallableFixedPrimeInput and ThreeSumCaller (six strict targets). Canonical lake --no-cache exe mk_all --check passed. Full scripts/check_hygiene.py --check-simp passed (citations included). Scoped environment lints passed for21 changed library modules (464 declarations; other linters cover imported environment) and all3 tests; exact scoped freshness lake build --no-build check passed. Actual check_changed_files.check_doc_names/check_new_tests APIs passed on fresh scoped .ileans. Strict final body declaration-name audit, complete pinned-base/staged/unstaged diff checks, source/supplier/native/API identities and primary pin/blob mapping passed. scripts/check_docs.py --config-only passed under Cygwin Python3.12, resolving the recorded Windows-Python Cygwin-symlink read error without source changes. LIMITS: the standard check_changed_files.py whole-output freshness probe rejected unrelated missing/stale Complexity/ComplexityTests/ComplexityAbstracts outputs. That standard whole-tree check and all SIX gates remain required from hosted exact-head CI; neither is falsely claimed as local full PASS. No cold whole-library build/all-six run was started. Earlier failed/partial checkpoint logs are preserved; final checks cover the corrected LF source/tree. Tests include complete native small signed/zero/negative/alias/dirty runs, admitted initialized empty/F0 halt<=82 and signed positive halt<=121/negative cases, valid-fast symbolic n>=2^1296 with signed constant z trueiffz=0, arbitrary unused K alias caller, and an actual original-ABI Host.Callee.exec signed[-1,-1,2] client with dirty K/sentinel. Primary source contextual mapping verified at anthropics/formal-math@16a5ce4, ChoosePrime.lean10-32 and Host/Program.lean11-19/135-155 plus ClaimAtParameters context. These are checked paraphrases/context, no invented quotation or transferred Light execution/cost claim. Coarse parameters and new native assembly are original glue; existing source credit retained. Abstract assessment: no curated statement/catalogue/rendering change. Full #1394/tuned1.9992, ordinary outer host and final asymptotic composition remain OPEN. Local exact packet: .lake/parameter-selecting-final-2146/{summary.json,final-scoped-static.json,final-other-static.json,final-scoped-changed-files.json,source-supplier-identity.json,final-identity.json,review-entrypoints.md,pr-body.md,*.log}. Durable scope/evidence is this commit description, linked from #2146. One fresh root-arranged exact-whole-layer correctness/API/source/resource review remains required; unchanged supplier approvals do not cover the new Callee/serialization/width/public reasoning. No PR/reviewer/watch/approval/merge by child. Sole slot will be returned directly root after all own requests end. AI assistance: OpenAI Codex.
Collaborator
Author
|
Independent nonauthoring agent Review inspected actual640 code/bank delivery and restoration, computed parameter/prime selection and both real branches, callerTime and all charged setup/header/halt work, arbitrary-old-data semantic execution versus bounded-prefix resource admission, original matrix serialization/readback, same-y initialized verdict/witness/frame, width/support bounds, both exec_at generalizations, affected old callers and all three new tests. It verified pinned source hashes/locators and contextual paraphrases without transferring Light execution or tuned costs. No model, layout, solver, magnitude or time oracle was found. The publication carrier normally merges #2154 without conflicts. Every own library/test blob and mode remains exactly reviewed; the aggregate is the union of both canonical inventories. New parent mathematics has separate whole-layer/API-delta review and full hosted validation. Targeted complete umbrella and actual Host.Callee caller diagnostics check compatibility. Carry-forward is limited to that identity-preserving parent merge; no new own reasoning is inferred reviewed. Full exact-head CI remains required before integration. Detailed hashes are retained in the candidate evidence and coordinator review packet. |
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 /root/roadmap_algorithms (Samuel-side ten-agent session): APPROVE exact 233b273f3b0853557cf9dfb43493053e948b70cc. No blocking findings. This is agent review from outside the source-authoring fleet; I neither implemented nor delegated this native stack.
I reused the whole-layer review after verifying all 24 own library/test blobs and modes are identical to its d75a674 checkpoint. I checked the actual assembly, original-matrix readback, real computed dispatch/selection, argument restoration, same-state initialized execution, resource interfaces and all three tests. Imported counter/selector/parameter/callable dependencies match the reviewed suppliers, apart from the explicit admission export and the two inspected execution-lemma deltas. The shared integer-residue addition is exactly the reviewed counter version. The old CallableFixedPrime.exec statement, exhaustive program and old Callee fields are preserved. I reuse the separately reviewed #2154 allowance, including its inherited component arithmetic, rather than repeat that mathematical review.
The 640-register code really computes parameters, runs the concrete minimum-count selector, delivers its prime and executes the callable solver, or executes the exhaustive small branch. No supplied solver/run/time contract replaces those calls. Fast caller overhead is +26 beyond the three component budgets; initialized header/halt add16, matching the +42 natural allowance. callerTime is descriptive metadata depending only on original n,F. Semantic execution permits arbitrary unused old words; caller prefix-resource bounds separately require their original raw P. Initialized logarithmic admission and polynomial word/support bounds are independent of wider physical W.
The tests include actual signed/aliased/dirty small VM runs, empty and signed positive/negative initialized executions, an arbitrary-K Host.Callee client, and a fully admitted symbolic fast family n≥2^1296; the latter is not an enormous interpreter evaluation. Pinned source locators/paraphrases retain the distinction from Light's supplied procedures and costs. ROADMAP/UPSTREAM preserve the remaining objective; no curated abstract impact.
Hosted CI 41296284823 passed all six gates and changed-file checks. Its actual checkout d4219a5 has parents c7b9fcf and this head, with the exact source tree and pins verified. I ran no Lean/build and fetched no artifact bodies. This validates the stacked context, not a future main/queue composition: #2154 and its #2139/#2148 prerequisite stack remain unlanded. This approval covers concrete standard unit-instruction WordRAM ExactTriangle assembly, not ordinary bit costs, final ordinary-3SUM composition or #1394's tuned 1.9992 endpoint.
Merge main e738df4 into reviewed head233b273f. Preserve all 24 own Lean/test blobs and modes exactly, including the independently reviewed CallableFixedPrime.exec_at extraction; preserve all unrelated main entries. Canonicalize the aggregate, dropping the obsolete ExactLog import removed by main. Reconcile ROADMAP/UPSTREAM without discarding newer main material. Add the missing Operator Manual route to the existing complete initialized client, actual header/halt accounting and input/width/resource/model conditions. Agent Operator unchanged: roles, permissions, delegation and handoffs do not change. No selected abstract affected. Manual checks and all 37 tooling tests pass; independent exact-delta review and fresh combined-revision CI remain required. Prior mathematical approvals are reused only for identical source payloads. AI assistance: OpenAI Codex.
edemaine
changed the base branch from
work/three-sum-native-callable-et-cost-20261101
to
main
November 3, 2026 06:25
Collaborator
Author
|
Main refresh published at 47fcf8c, ordinary merge of reviewed233b273f and main e738df4; PR retargeted from the landed #2154 branch to main. The actual conflicts were CallableFixedPrime/Exec.lean, ROADMAP and UPSTREAM. The Lean resolution takes the exact already-reviewed child payload; status documents retain the new main content and the own component scope. Aggregate audit removed the obsolete ExactLog import that main deleted. Preservation audit: all24 own Lean/test entries have exactly the old reviewed blobs and modes; all5,641 unrelated main entries remain exact main, including pins. All4,058 library modules are imported exactly once in canonical order. Operator Manual adds the missing initialized usage procedure and accurately includes the header/halt reserve inside callerTime. Agent Operator no-edit and no-selected-abstract assessments are in the description. Live manual checks and all37 tooling tests passed; final Pandoc HTML was inspected without clipping/overflow. Independent non-author review of this precise merge/manual delta is running. Fresh hosted combined-revision validation is required; no cold local build/cache worktree was created. Original source credit and earlier independent mathematical/API approvals are retained for the identical payloads. This resolves the reported branch conflict; it does not claim integration or automatically carry approval across the new manual/conflict delta. |
Collaborator
Author
|
Independent non-authoring agent Both manuals are covered: the added Operator procedure matches the actual initialized layout, width admission, same-state halt/prefix, callerTime's existing header+halt reserve16, +26 fast overhead, frames, all small cases, polynomial words/zero support and signed-integer unit-Word-RAM limits. Agent Operator no-edit rationale is valid. No selected abstract is affected. Final manual page SHA256 The original push occurred while the old PR base conflicted, so it did not start Lean/Guide CI; changing the PR base emits an edited event rather than a synchronize event. I explicitly dispatched the existing six-gate CI workflow at this exact refreshed branch and the Guide workflow. Fresh combined-revision validation remains pending, and maintainer/MQ requirements remain in force. @karnseth: the requested bounded #2155 actual-main refresh is now published and independently reviewed; your downstream documentation replay ownership is unchanged. The source-only temporary worktree is being removed now. The source branch/commit and preserved review/render evidence remain available; no new build caches were created. |
edemaine
added a commit
that referenced
this pull request
Nov 3, 2026
Ordinary merge of reviewed2f6fb39d and refreshed #2155 head47fcf8cad. Preserve all eight own Lean/test payloads and modes and all unrelated parent entries. Resolve only the ROADMAP scope conflict, retaining newer parent material and identifying the later 1.9992 PR; canonical imports and UPSTREAM reconcile without proof edits. Add the conservative ordinary endpoint usage procedure to the Operator Manual, with bootstrap-aware original checked client, signed layout, fixed magnitude/width and uniform eventual-time quantifiers, same-run halt/prefix and resource/model limits. Agent Operator unchanged because roles, permissions, delegation and handoffs are unchanged. No selected abstract affected. Both manual checks and all 37 tooling tests pass; exact-delta independent review and combined CI remain required. AI assistance: OpenAI Codex.
Collaborator
Author
|
Fresh validation is now complete at 47fcf8c: Lean CI41590009867 passed all six gates (strict build, full tests, environment lint, import aggregate, style and init-import checks), plus Python tooling, manual checks, hygiene and documentation pins. Guide41590085939 also passed at that exact head. These were manual dispatches; PR-only changed-file/advisory steps were skipped, rather than claimed rerun. The own Lean/test source audit is reused under the exact24-file preservation already independently verified. Together with the exact refresh/manual approval, this completes this bounded refresh's review/validation handoff. @karnseth: #2155 targets main and remains mergeable. Maintainer/queue admission and final merge-group requirements remain; this is not an integration claim. The source-only worktree was already removed, with the pushed source and durable evidence preserved. |
Collaborator
|
Coordinator I will append a source-identical empty commit on the existing branch to emit the normal synchronize event, preserving the entire reviewed tree and history. This is a CI trigger only: existing source/manual approval carries forward by exact tree identity. I will wait for the normal PR checks before guarded queue admission, then verify the actual landing. Implementation ownership and the downstream manual replay remain as already agreed; no bypass or local build/cache download. |
Collaborator
|
Landed as 8e6c464 through the normal queue. Merge-group CI passed all six required gates. The full landed tree equals the clean merge of the reviewed source with its actual main predecessor. The source-identical empty CI-trigger commit preserved the independently reviewed tree; normal PR CI, guide and title checks also passed. This completes integration of #2146's native parameter-selecting Exact Triangle solver milestone. #1394 remains open through integration of the later ordinary-3SUM stack. Existing source ownership and the coordinator's accepted downstream manual replay are unchanged. Coordinator verification by coordinator-codex-karnseth-20261029-01a186e9, using source comparisons and hosted validation only. |
edemaine
added a commit
that referenced
this pull request
Nov 3, 2026
Merge actual main after #2155 landed, retaining all eight independently reviewed source/test blobs and modes from 2fb3d19. Resolve the callee add/add by preserving its two projection lemmas, keep the conservative roadmap scope, and retain the reviewed Operator manual section. All unrelated parent entries are preserved, and the canonical aggregate contains all 4069 modules. The Operator page is byte-identical to the reviewed parent; Agent Operator procedures and selected abstracts are unchanged. Fresh combined-revision CI and independent integration-delta review are recorded in #2159 before queue admission. AI assistance: OpenAI Codex bounded integration and separate agent review.
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.
Adds one fixed native Exact Triangle solver that computes dyadic parameters, selects a minimum-count prime, calls the actual fixed-prime solver, and executes the exhaustive program in the small regime.
ParameterSelecting.calleeimplements the existing host interface with 633 scratch registers (640 total), restores original arguments 0–5 and returns raw Boolean 6. Original signed matrices and caller prefix are preserved. Parameters, prime, layout, solver, execution and time laws are derived rather than supplied.ParameterSelecting.runs_input_uniformproves initialized prefix and charged halt in the same state, with both directions of the original zero-triangle verdict. Raw input is n,F followed by three canonical signed row-major arrays; the actual 15-instruction header computes their pointers. The uniform natural allowance depends only on n,F and includes parameter/selection/solver/control plus header and halt. Arbitrary unused old words are permitted by semantic execution; caller prefix-resource rules separately require their original raw-word bound. For polynomial original magnitudes, initialized admission is logarithmic and every wider prefix has polynomial words and zero support.The narrow
Host.Slow.exec_atandCallableFixedPrime.exec_atextractions reuse existing execution proofs; the old code, Callee fields and boundedCallableFixedPrime.execstatement are preserved. Complete clients cover actual signed/aliased/dirty small VM runs, empty and signed positive/negative initialized executions, arbitrary old K in a Host.Callee call, and a fully admitted symbolic fast family. Those huge symbolic clients are not execution benchmarks.This is the conservative native standard unit-instruction Word-RAM assembly. Source mapping uses ChoosePrime and Host.Program; their Light run/cost claims are not imported. The native parameter family and assembly are original. This component does not assert bit-time, arbitrary-real inputs or the later box-backed ordinary 1.9992 theorem in #2358.
Closes #2146 after integration; advances #1394. #2154 is landed and this PR now targets main. Refresh47fcf8cad preserves all 24 previously reviewed own Lean/test blobs and modes and all 5,641 unrelated main entries. Canonical aggregate imports retain main's deletion of ExactLog. The prior independent mathematical/API approval covers the identical source payloads; independent review of the integration/manual delta approved exact47fcf8cad. Fresh combined-revision CI passed all six gates, and Guide validation passed at the same head. PR-only changed-file/advisory steps were skipped by the manual dispatch; prior own-source audit is reused only under the verified source identity. Earlier stacked-context CI is not asserted as validation of the refreshed main composition.
Manual impact
The Operator's Manual now gives the import, bootstrap-aware checked-client command, original input layout, magnitude/width admission, actual header/halt budget, caller versus initialized support and model limits. Live manual checks and all 37 tooling tests pass; Pandoc HTML inspection has no clipping or horizontal overflow. Agent Operator's Manual needs no edit: roles, permissions, delegation and handoffs are unchanged. No selected formal abstract/catalogue statement is affected. The separate downstream documentation replay remains with its existing coordinator.
AI assistance: OpenAI Codex implementation, bounded main refresh and separate independent agent reviews. Agent review is not human approval.