Formula-phase space bound for one direct transition step

This module follows the exact state, head, and cell formula trajectories and certifies every nested routine against the shared packed-step width envelope.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepFormulas_spaceBoundByWidth_internal {k : ℕ} (tm : NTM k) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), StepClean (values inputLength)) (hhorizon : ∀ (inputLength : ℕ), 0 < values inputLength Work.horizon) (henvelope : ∀ (inputLength : ℕ), StepWidthEnvelope tm (values inputLength) (width inputLength)) : (emitStepFormulas tm).SpaceBoundByWidthAt initialSpace values width

The complete forward formula phase stays within the shared width envelope.