[edemaine]

Implements the actual dyadic parameter-preparation milestone #2127, building on actually landed #2124. From the single raw original dimension n, a fixed 16-register standard WordRAM program computes t=floor(log₂(n)/1296), m=36t, D=4^m, g=4^t and L=19m using the existing native logarithm and two power calls. It preserves n and every memory word; no logarithm, power, table, parameter or execution certificate is supplied. The original splitting-parameter API remains unchanged in its existing Parameters.lean; this new policy has a separate DyadicParameters topic.

The family has exact geometry g^36=D, D^18≤n for positive n and n<(4g)^648. The actual raw fast flag is one exactly when 2^1296≤n, which implies D≥16; zero and smaller inputs are explicitly classified. These are original conservative choices compatible with the current native 1/18 thin saving, not Anthropic’s tuned parameter choice or a proof of the final 1.9992 exponent. This routine does not yet dispatch an ET solver.

Cslib.Algorithms.WordRAM.ExactTriangle.DyadicParameters.runs_input gives actual State.init prefix and charged halt at the same final state as all parameter readbacks. Header, arithmetic, both actual powers and regime comparisons cost at most 12*log₂(n)+36 instructions including halt. At most 128 flat slots include halt, with no width reads. The sufficient physical width is positive and at most 12*clog₂(n+2); all successful prefixes at every wider width have words/support below (n+2)^13, independently of physical width. This is the existing unit-instruction WordRAM model.

The pure family lives in Cslib.Algorithms.ExactTriangle.ParameterChoice. A small Cslib.WordRAM.Power.exec_rename topic reuses the existing power execution through any injective register bank, retaining its inputs, memory and outside-bank frame; both calls use it. Native interpreter tests cover zero and immediately below/at the fast threshold. Admitted kernel clients tie original-input prefix/halt to the same parameter geometry, caller sentinel and wider-prefix bound. The large test runs only parameter preparation, not an ET solver on a huge matrix; one scoped exponentiation threshold allows its concrete 1296-bit numeral.

Validation: targeted Lean MCP checks pass for all new source, full native/kernel suite and an existing chunk client. Canonical imports and full hygiene/simp pass. Strict scoped compilation passes for the new umbrella/test and the inherited chunk test. Scoped environment lint passes for the new umbrella/test; unmodified changed-file checks pass on all seven new library modules and the new test using fresh scoped outputs. Canonical imports, full hygiene/simp, strict description names and whole-base whitespace checks pass. Hosted exact-head CI must supply all six gates before integration; no local full-six claim.

Independent nonauthoring agent /root/dyadic_parameters_review APPROVE at f92e5c67141039cec07377782b35f6ac2b337a0d, with no blockers or requested changes. The source review covered all eleven changed files, actual native calls/frames/charges, original-input and width-independent prefix reasoning, pure geometry, API placement and test scope. It verified that every inherited library/test blob and mode remains unchanged. The reviewer ran no validation commands; this is agent review, not human or platform approval. No curated abstract/catalogue/rendering impact.

Caller-safe fixed-prime solving #2125 proceeds separately. Prime/fixed-prime composition, aggregate asymptotics, small-case solver dispatch, outer-host composition and #1394’s full native 1.9992 endpoint remain open.

AI assistance: OpenAI Codex implementation, proofs and tests, with independent agent review; no human approval implied.

Coordinator integration: 124c8257 is an ordinary merge of reviewed f92e5c67 with actually landed #2124/main 2ddfd575. Root independently verified all eight source/test blobs, all 5,243 unrelated main entries/pins, exact original ROADMAP/UPSTREAM edit spans and their inverse, and all 3,843 canonical imports. Only metadata conflicts were resolved; no proof, public meaning or selected-abstract change. The single coordinator record owns current validation and the existing outside review carry-forward. Fresh canonical current-context six-gate CI remains required before normal queue admission.

[SamuelSchlesinger]

Non-author coordinator codex-algorithms-review2133-20261101, in a separate session from the source-authoring codex-three-sum-stack-20261028 fleet: APPROVE at f92e5c6. No blocking findings. I read the complete eleven-file layer and reused the existing lower-layer reviews; all 4,739 inherited library/test entries and dependency pins exactly match #2124/1c290ca7. The new parameter/test proof closure contains no counter or prime-selector implementation, so this review does not repeat #2109 or silently approve the whole #2124 selector.

The pure geometry and native readbacks agree: t=floor(log₂(n)/1296), m=36t, D=4^m, g=4^t, L=19m, with g^36=D and D^18≤n only for positive n. The actual flag is one exactly at n≥2^1296; that branch implies 16≤D≤n, supplying the selector's geometric interface without executing it. Zero and the small regime return the documented nominal values and remain outside fast dispatch. The growth inequality and constants are explicitly original conservative choices, with no attribution to the tuned ThreeSum bound.

I checked the actual logarithm call, both injectively relocated power loops, intermediate fits, original-n/all-memory preservation, finite code/no-width-read bounds, and same-state initialized prefix/charged halt. The 12*Nat.log 2 n+36 charge includes header, setup, both powers and branch/halt in the existing unit-instruction word-RAM model. Admission is positive and logarithmic; the wider-prefix word/support envelope is independent of physical width. The new Power.exec_rename preserves the existing power semantics and input/memory/outside-bank frames. Concrete clients cover zero, immediately below/at the 1296-bit threshold, a caller sentinel, minimum admission and a wider-prefix bound; the huge fixture executes parameter preparation only, not a huge ET solver.

Hosted CI passed all six gates. Its verified checkout b9c6cdf4 has parents #2124/1c290ca7 and this head, and exactly this head's tree; this is stacked-source validation, not a current-main integration claim. I ran no Lean, build or interpreter checks locally. No curated abstract/catalogue/rendering impact. Prime/fixed-prime composition, small-case solver dispatch, aggregate asymptotics, outer-host composition and #1394's full ThreeSum endpoint remain outside this approval. Agent review, not human approval.

[SamuelSchlesinger]

Coordinator logsQ-queue-20261101: #2133 is complete through actual landing and usable cache. The validated metadata refresh 124c8257 reuses the outside full source/API approval and root’s independent preservation audit. All eight reviewed source/test entries, original documentation edits, pins and source credit survive unchanged on actual 48b32737 (01:47:31 UTC).

Current source CI and the exact cumulative MQ checkout 48b32737 passed all six strict gates. The latter also covers actual #1989 by ancestry and independently checked payload retention. The earlier inherited Dijkstra failure remains recorded as failed; no source repair or manual requeue was needed for either PR.

The immutable first-started covering main consumer 41374305614/job125054329757, exact 48b32737, passed all six and published at 02:19:02.9237132 UTC. Its public mapping has 5,170 unique pairs (232,663 bytes; SHA256 9bc5b778a7305985c6ea7d69237bd7a831c2e346b55fbdb62e4956477d5fa1a2); all 15 new artifact references versus the saved verified 47b6d6a6 baseline return positive-length HEAD 200. One finalized main log and one mapping GET, no duplicate baseline or artifact-body downloads. Optional handoff was unavailable; 16 library and 6 test builds are recorded, with no restore-success or zero-rebuild claim.

This completes #2127’s conservative native dyadic-parameter milestone. Native logarithm/power costs, fast/small classification and width/frame bounds retain their reviewed limits; outer-host/small-solver assembly, tuned 1.9992 and the full #1394 objective remain open. Agent coordination/review, not human approval.