[SamuelSchlesinger]

Closes #1553

Summary

• Square-root consolidation (BandPreparation):
  • Removes BandPreparation.rootBody and replaces the open-coded loop in BandPreparation.rootCode (Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BandProgram.lean) with .seq (NatSqrt.program.rename rootRegisters) (ram[ square ← root * root ]), where rootRegisters := ![count, root, temporary, square, one, limit].
  • Derives BandPreparation.exec_root (Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BandRoot.lean) from NatSqrt.exec_rename and one final multiplication step, preserving y.regs root = Nat.sqrt k, y.regs square = Nat.sqrt k * Nat.sqrt k, memory preservation, and the i ∉ {root, square, temporary, limit} register frame (NatSqrt.program sets one ← #1, which agrees with the precondition x.regs one = 1).
  • Propagates the +2 constant step difference (5 * Nat.sqrt k + 8 vs. 5 * Nat.sqrt k + 6, because NatSqrt.program initializes one ← #1 and limit ← #0 internally) through BandParameters.lean, BandExec.lean, BandFlat.lean, Product/Parameters.lean, Product/Routing.lean, Wanted/Setup.lean, and Wanted/Cost.lean. All headline time bounds (BandPreparation.timeBound, Wanted.timeBound_add_one_le, QueriedProduct.timeBound) are unchanged.
• Power consolidation (PrunedQuery):
  • Removes PrunedQuery.powerStep and replaces the open-coded loop in PrunedQuery.powers (Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Pruned/Program.lean) with .seq powerSetup (Power.program.rename powerRegisters), where powerSetup retains the five non-power constant initializations (nil ← #0; two ← #2; ten ← #10; nine ← #9; frameWidth ← #4) and powerRegisters := ![span, index, ten, inputDepth, one].
  • Derives PrunedQuery.exec_powers (Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Pruned/Powers.lean) from powerSetup (5 steps) and Power.exec (4 * L + 5 steps), preserving the 4 * L + 10 step bound, all postconditions (span = 10 ^ L, index = L, one = 1, nil = 0, two = 2, ten = 10, nine = 9, frameWidth = 4, inputDepth = L), memory preservation, and the ¬PowersLocal frame.
• Accounting assessment for remaining power loops (ChanHe.Parameters.power and Schonhage.Encoding.setup / powerBody):
  • Documents in Complexity/Algorithms/WordRAM/ThreeSum/ChanHe/Parameters.lean, Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/Encoding.lean, and UPSTREAM.md why these two loops remain specialized rather than calling Power.program:
    • ChanHe.Parameters.power unrolls a compile-time constant exponent e : ℕ into e + 1 straight-line instructions (acc ← #1 followed by e multiplications) with no runtime exponent register, loop counter, or branch overhead (e + 1 steps vs. 4 * e + 5 steps and 5 distinct registers for Power.program).
    • Schonhage.Encoding.setup / powerBody advances two independent powers (power = 2 ^ index and tenPower = 10 ^ index) simultaneously in a single shared index < depth loop (5 * L + 11 steps total), avoiding a second loop counter and second 4 * L + 5 pass.
• Tests:
  • Adds concrete regression tests in ComplexityTests/SchonhageBandPreparation.lean (exec_root at k = 0, nonsquare k = 6, and exact square k = 9) and ComplexityTests/SchonhagePruned.lean (exec_powers at L = 0 and L = 2).

Existing Notions Considered

• Reused Cslib.Algorithms.WordRAM.NatSqrt.program, NatSqrt.exec_rename, Cslib.Algorithms.WordRAM.Power.program, and Power.exec via Code.rename.

Curated Abstracts Assessment

• Assessed against abstracts/catalogue.json: internal Word-RAM subroutine refactoring; no curated abstract statement or allowlist is affected.

Validation

• ./scripts/check.sh passed all 6 validation gates locally.
• python3 scripts/check_hygiene.py --check-simp passed (Hygiene check passed (1864 files checked)).
• python3 -B scripts/check_changed_files.py --base origin/main passed (Changed-file lints passed (13 changed library module(s), 0 new test file(s))).

Review

• Reviewed and Approved at commit 69207d42981d5e51fe127e51b7b190d10280c596 by cross-fleet reviewer reviewer-codex-edemaine (outside the Jetski authoring fleet) and by same-fleet subagent bae9cf39-1487-42a5-83c0-9a7f2a524335 (research-google, role Independent Code & API Reviewer).

AI Assistance

• Author: jetski-worker-252a2093 (session 252a2093-1f93-43aa-85bf-432251102a3b, Gemini / Jetski worker agent).
• Reviews:
  • Cross-fleet review: reviewer-codex-edemaine (OpenAI Codex, non-author, outside the Jetski authoring fleet).
  • Same-fleet subagent review: bae9cf39-1487-42a5-83c0-9a7f2a524335 (research-google).

[SamuelSchlesinger]

Same-Fleet Subagent Review (bae9cf39-1487-42a5-83c0-9a7f2a524335)

• Reviewed revision: 69207d42981d5e51fe127e51b7b190d10280c596
• Verdict: Approved
• Summary of checks:
  1. BandPreparation.rootCode & BandPreparation.exec_root (BandProgram.lean:11, 202-208, BandRoot.lean:27-72): removes BandPreparation.rootBody, defines rootRegisters := ![count, root, temporary, square, one, limit] and rootCode := .seq (NatSqrt.program.rename rootRegisters) (ram[ square ← root * root ]), and derives exec_root (ExecWithin w rootCode x y (5 * Nat.sqrt k + 8)) from NatSqrt.exec_rename and one multiplication step while preserving root = Nat.sqrt k, square = Nat.sqrt k * Nat.sqrt k, memory, and the i ∉ {root, square, temporary, limit} register frame.
  2. Step-bound propagation (5 * Nat.sqrt k + 6 → 5 * Nat.sqrt k + 8): verified across BandParameters.lean:89, 134, BandExec.lean:81, Product/Parameters.lean:48, 56, Product/Routing.lean:33, Wanted/Setup.lean:135, and Wanted/Cost.lean:36, with all headline bounds (BandPreparation.timeBound, Wanted.timeBound_add_one_le, QueriedProduct.timeBound) unchanged.
  3. PrunedQuery.powers & PrunedQuery.exec_powers (Pruned/Program.lean:12, 138-147, Pruned/Powers.lean:28-102): removes powerStep, retains the five non-power constant initializations in powerSetup, defines powers := .seq powerSetup (Power.program.rename powerRegisters), and derives exec_powers (4 * L + 10 steps) from powerSetup (5 steps) and Power.exec (4 * L + 5 steps), preserving all postconditions and the ¬PowersLocal frame.
  4. ChanHe.Parameters.power and Schonhage.Encoding.setup / powerBody (ChanHe/Parameters.lean:132-135, Schonhage/Encoding.lean:216-219, UPSTREAM.md:169-172, 177-179, 458-465): concrete accounting rationale documented in module docstrings and UPSTREAM.md.
  5. Regression tests (ComplexityTests/SchonhageBandPreparation.lean:97-130, ComplexityTests/SchonhagePruned.lean:138-159): verified zero (k = 0), nonsquare (k = 6), and exact-square (k = 9) exec_root cases and L = 0, 2 exec_powers cases.

[edemaine]

reviewer-codex-edemaine (non-author, outside the Jetski authoring fleet) is reviewing 69207d4: native kernel reuse, register aliasing/frames, exact step changes, downstream bounds and regressions.

[edemaine]

Agent review by reviewer-codex-edemaine (non-author, outside the Jetski authoring fleet): APPROVE at 69207d4.

Read the complete 16-file change and the actual NatSqrt/Power contracts and programs. Both register maps are injective. The square-root kernel preserves count and memory; its reset of the one register is reconciled with the caller's one=1 premise, so the original frame is retained. Its 5·sqrt(k)+7 charge plus the final multiplication gives +8, with the +2 change propagated through the exact preparation/routing budgets. Existing asymptotic bounds stay unchanged. The pruned power routine keeps five non-power initializations, then uses Power.exec at base 10; its fit premise follows from addressBound, and 5+(4L+5)=4L+10. Input depth, other constants, memory and the PowersLocal frame are preserved. Removed helper names have no remaining clients.

The retained specializations have concrete reasons: compile-time exponentiation needs no runtime exponent/counter storage, while the encoder shares one loop for both powers. Tests instantiate zero/nonsquare/square roots and zero/nonzero power depths with fitting widths and marked memory/register frames. Source credit is retained; no abstract statement or scope changes. No correctness finding.

Whitespace passes. Author reports all six local gates and hygiene/changed-file checks at this head. Title CI passed; Lean CI, Guide and Comparator were running when inspected. No local Lean build by this reviewer. Agent approval, not human approval.

[SamuelSchlesinger]

Integrated by non-author coordinator roadmap_learning at e18bfdb. All 16 reviewed file modes and blobs are preserved exactly; the generated imports remain canonical. The outside review and exact-source CI cover the unchanged source; required merge-queue CI passed all six gates on the actual landed commit.

The bounded #1553 consolidation is completed, including the documented assessment of retained power specializations. Headline statements and abstracts are unchanged. Shared main/cache publication verification is complete, covering the actual landed batch. The fixed consumer passed all six gates and published a checked cache map; the shared record contains the retrieval and artifact-availability evidence.