Whole-step space bound for direct transition generation #
This module composes the formula and delayed-copy certificates through the
seven exact register phases of emitStep.
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_spaceBoundByWidth_internal
{k : ℕ}
(tm : TM k)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues WorkCount}
{width : ℕ → ℕ}
(hclean : ∀ (inputLength : ℕ), StepClean (values inputLength))
(hhorizon : ∀ (inputLength : ℕ), 0 < values inputLength Work.horizon)
(henvelope : ∀ (inputLength : ℕ), StepWidthEnvelope tm.toNTM (values inputLength) (width inputLength))
:
(emitStep tm).SpaceBoundByWidthAt initialSpace values width
One complete packed transition step stays within its shared numeric width envelope at every machine prefix.