Packed-copy space bound for one direct transition step

This module certifies the delayed-copy suffix after the next-formula stream has been emitted. The proof follows the exact rolling formula cursor through the state, head, and cell regions and bounds every loop prefix by the shared step width envelope.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepPackedCopies_spaceBoundByWidth_internal {k : ℕ} (tm : NTM k) {initialSpace : ℕ → ℕ} {baseValues values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), StepClean (values inputLength)) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (henvelope : ∀ (inputLength : ℕ), StepWidthEnvelope tm (baseValues inputLength) (width inputLength)) (hhorizonEq : ∀ (inputLength : ℕ), values inputLength Work.horizon = baseValues inputLength Work.horizon) (hgateCount : ∀ (inputLength : ℕ), values inputLength Work.gateCount = baseValues inputLength Work.available) (havailable : ∀ (inputLength : ℕ), values inputLength Work.available = baseValues inputLength Work.available + stepFormulasEffectSizeInternal tm (baseValues inputLength Work.horizon)) : (emitStepPackedCopies tm).SpaceBoundByWidthAt initialSpace values width

The delayed packed-copy phase stays within the shared width envelope.