[petalas]

Summary

Prove the exact positive moving-Gaussian stage count when the word must restore its whole-block permutation internally. Claim type: scoped mathematical proof with exact finite corroboration.

E_s = P_(0,s) D_0, including E_0 = D_0
k requested nonanchor blocks, anchor parity b in {0,1}
minimum stages = 2k + ((k+b) mod 2)

Unused spectator blocks cannot reduce the count. Requesting all three blocks requires five stages. The attaining word doubles every requested nonanchor stage and uses at most one anchor stage. Its residual block-local monomial is explicit and remains part of the output contract.

Cinna Davis / 1337isnot1337's #5113 supplies the moving-coordinate interface. Chris R / Clear1nsight's #5133 uses a three-stage word whose output accepts an external block permutation. The present theorem changes that return requirement; it does not audit either predecessor or dispute their claims. Retain Dillon #4933, Dugongue #4929, Cao Yifan, Cayden Burkart, JoyboyBrian, zxv, Jacob Alan Sussman and the native/compiler/precision lineage credited through #5113. The new theorem, proof and verifier are produced by Nick Petalas. Independent human and formal proof-kernel review are unclaimed.

Evidence

The written proof applies to every positive block width and every finite spectator count. Independent shortest-path enumeration covers all 50,362 quotient states and all 126 permutation-restored endpoints through six blocks. A separate literal finite-field interpreter checks 916 operator columns, including two-axis blocks and the residual local monomial. Twelve malformed-input and endpoint controls pass. No predecessor executable is imported.

The source's three-stage externally normalized boundary remains available. Under the new internal-return boundary, the shortest-path oracle returns five stages, matching the attaining word and the lower bound. This comparison concerns different boundaries, not a predecessor defect.

From the repository root, CPython 3.12.15 and the standard library:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/moving-stage-restoration-tariff/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/moving-stage-restoration-tariff/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/moving-stage-restoration-tariff
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/moving-stage-restoration-tariff --check-source-history --check-modes

Expected scientific marker: PASS_MOVING_STAGE_RESTORATION_TARIFF. The registered normal and optimized commands passed locally, timed individually at 0.16 and 0.17 seconds. Metadata, source pins, committed bytes/modes and full source-history checks passed at 26b1c960e0510593e5e541af7f830efad504f15e. The official eight-file export passed integrity and declared-input coverage checks; its optimized verifier also passed outside a Git checkout. A generated local receipt binds all six package hashes.

Limitations

This is a stage-count theorem in the stated positive alphabet and Gaussian-parity quotient. Block-local monomials remain explicit. Full monomial cleanup, physical movement, main-owner independence, helper targets, native/caller/compiler, precision and outer invoices are unpriced. The executable oracle is bounded to six blocks; the all-width result rests on the written proof. No selected cold replay, Lean proof, complete supplier, new kappa or complete multiplication theorem is claimed. The selected frontier is unchanged.

Open next questions

• Compare internal restoration against an external block permutation in one actual complete caller, charging all stages, residual monomials and productive target changes.
• Fix a stricter endpoint and inverse-stage policy, then determine the exact minimum when every local monomial must also disappear.

Related open work

Completion refresh covered this account's nine other open PRs created since the advance CLAIM: #5982 through #5990. None studies this positive moving-stage internal block-return boundary, and no shared numerical result is compared. Merged #5113 and #5133 remain the credited predecessors. Unpublished work is outside this coverage.

CI notes

Both hosted checks passed at 26b1c960e0510593e5e541af7f830efad504f15e: plan and replay (research/moving-stage-restoration-tariff), in run 40570275996. The completed check list was read once, and the run head matches the PR head. The registered normal and optimized replay is now CI-certified; independent human or proof-kernel acceptance and the out-of-scope supplier obligations remain unclaimed.

Merge Danger

Two-way door. Changes are confined to the new research package and can be reverted independently.