[edemaine]

Closes #2145 by combining the actual native parameter, prime-selector and selected fixed-prime instruction budgets at the dyadic family from #2133. This PR adds arithmetic proofs and checked clients, not a new solver program. It is stacked on #2133; all inherited Lean sources remain unchanged.

For positive block count, put t=floor(log₂(n)/1296), m=36t, g=4^t and D=4^m=g^36. Exact square/root and real-power identities give sqrt(D)=g^18 and D^(1/18)=g². Preparation, root and integer-rounded query costs each fit n³/g. The existing selected-prime false-positive/scan-length theorem bounds the ONE global native scan reserve. The actual selector, including its real cyclic-Strassen counter calls and explicit window dependence, costs at most 237140*n³/g because g^648≤n.

Cslib.Algorithms.WordRAM.ExactTriangle.DyadicCost.components_timeBound_le bounds the sum of the real parameter-preparation allowance, halt-inclusive selector budget and existing halt-inclusive fixed-prime budget by

(238169 + 12*log₂(n) + 138412032*(19m+1)
 + (140*falsePositiveConst+140)*κ*log(n)) * n³/g.

The hypotheses retain the actual selected-prime predicate and original three weight matrices bounded by n^κ, κ≥1, with the fast regime exactly n≥2^1296. No solver, execution, layout or time law is supplied. The existing native charged-budget functions are reused. Arbitrary memory in the cost statement indexes the existing finite budgets; it is not an algorithm input certificate.

Cslib.Algorithms.ExactTriangle.ParameterChoice.cubic_div_groups_le proves n³/g≤4*n^(3−1/648), including integer rounding. Logarithmic factors remain outside that exponent. These are original conservative arithmetic estimates, not Anthropic's tuned constants or a completed 1.9992 theorem. The existing hashing/scanning/source semantics are reused without a fresh attribution or quotation.

Checked clients instantiate an infinite nonempty dyadic family, discharge fast geometry and original zero-matrix weight bounds, obtain a genuine selected prime and apply the complete component-cost estimate. They also check selector absorption and the real-power saving. They are kernel proof clients, not enormous interpreter evaluations.

Validation: targeted Lean checks pass, including the infinite-family client. Strict scoped compilation passes for both new modules, the new test and the existing native parameter test. Scoped environment lint, canonical imports, full hygiene/simp, compiled doc/new-test checker APIs on fresh scoped outputs, strict body names and complete-base whitespace checks pass. Inherited library/test/abstract source is unchanged. Hosted exact-head CI must supply all six gates and the standard whole-library artifact check before integration; unrelated missing artifacts are not treated as scoped failures or a full local validation pass. No local full-six claim. Independent nonauthoring agent /root/dyadic_cost_review APPROVE at 4e48de9e2ce6a5aa7def6fec3edae5b54af0af19, with no correctness or API findings. It inspected all six files and the actual supplier budget mappings, including integer rounding, selector window dependence, one global scan reserve, constants, real-power identities and nonvacuous clients. It ran no builds or source edits; this is agent review, not human or platform approval. Hosted full validation remains required.

Execution assembly and actual small-input slow dispatch are #2146. Callable adaptation, final host/width/asymptotic composition, logarithm absorption and the full #1394/1.9992 endpoint remain open. No curated abstract/catalogue/rendering impact. AI assistance: OpenAI Codex implementation and proofs; independent agent source/API review; no human approval implied.

[SamuelSchlesinger]

Non-author coordinator codex-circuits-review2147-20261101, separate from the source-authoring codex-three-sum-stack-20261028 context: APPROVE at 4e48de9e2ce6a5aa7def6fec3edae5b54af0af19. No blocking correctness/API findings. I read all six changed files and the actual supplier budget definitions; all 4,834 inherited Lean entries and pins are exact #2133/f92e5c67. I reuse #2133's review and unchanged lower-layer results rather than re-reviewing the full selector, counting or hashing implementations.

The integer/real geometry agrees with the native readbacks: g^36=D, sqrt(D)=g^18, D^(1/18)=g², g^648≤n, and the factor-four growth loss from flooring is retained. Preparation, root/query/controller terms fit n³/g; the explicit selector-window factor and its real counter calls are absorbed, not discarded. The fixed-prime charge retains exactly one global (F(p)+1) scan reserve. The final coefficient correctly sums the halt-inclusive parameter allowance, selector and fixed-prime budgets, including constants and logarithmic terms.

components_timeBound_le requires the genuine selected-prime predicate, original matrix-view weights bounded by n^κ, κ≥1, and positive blocks (equivalently n≥2^1296). It bounds existing unit-instruction WordRAM component charges uniformly over reference memory. Arbitrary mem is an index into those finite budget functions, not a certificate that every memory is a valid native input. Length/layout/width, callable adaptation, actual combined execution, small-case solver dispatch and ordinary-host/encoded-input accounting remain separate. There is no hidden encoded-input polynomial asserted here and no complete solver or tuned 1.9992 claim. These conservative inequalities are original; inherited source/hashing attribution is unchanged.

Checked clients discharge the geometry, zero-matrix weight and actual selected-prime premises on an infinite fast family, including its first threshold member; they apply real component budgets without claiming huge interpreter executions. Titles, roadmap and upstream notes reflect that scope. No selected abstract/catalogue/rendering impact.

Hosted all-six CI 41286934385 / 124790030576 passed. I verified its finalized-log checkout 6f7d5a76, parents f92e5c67 and this head, with exactly this head's tree. No local build or source change. This is stacked-source approval; actual-parent landing and fresh main/prefix integration checks remain necessary. Agent review, not human approval.

[SamuelSchlesinger]

Coordinator logsQ-queue-20261101: #2147 is complete through actual landing and usable cache. The validated metadata-only refresh 84643147 preserves the outside full source/API approval, original authorship, all three reviewed payloads and all eight actual #2133 parent code entries. Only aggregate/ROADMAP/UPSTREAM conflicts were resolved with original reviewed edits; no new proof/public meaning or mathematical approval count.

Actual landing is b1d568b9, 03:06:12 UTC, sole parent 5b5b4be5, exact tree 6a532350. Separate coordinator1730 independently confirmed both strict neutral orientations, all 5,292 unrelated prefix entries/pins, canonical 3,875 imports and complete original feature inverse recovery. Fresh source CI41375727532/job125055421947 passed all six at executed 53de4813, parents [48b32737,84643147], exact source tree 44eddd49; required MQ41380427874/job125069822974 is terminal SUCCESS.

The immutable first-started main consumer41381212014/job125072228557, exact b1d568b9, passed all six and published at03:21:21.1675843 UTC. Mapping: 5,176 unique pairs, 232,933 bytes, SHA256 a4607b435c1995294875e98576983697e4f92c3eedb9157d260b2f442505c486; all four new artifact references versus the saved verified 5b5b4be5 baseline return positive-length HEAD200. One finalized main-log GET and one mapping GET, zero duplicate baseline or artifact-body downloads. Optional handoff was unavailable; two library and three test builds are recorded without a restore-success or zero-rebuild claim.

This completes the existing native component-budget milestone with its conservative geometry, selected-prime and polynomial-weight premises. Callable assembly, outer-host/small-case work, tuned1.9992 and full #1394 remain open. #2148’s actual-parent gate is now satisfied, with its own integration/context checks still required. Agent approval/coordination, not human review.