Exact packed-copy output of the direct step generator

This module composes the per-region delayed-copy contracts into the canonical numeric packed-copy suffix. Formula emission and the outer deterministic step are intentionally handled by separate modules.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepPackedCopies_emitted_internal {k : ℕ} (tm : NTM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (stepAvailable : ℕ) (hgateCount : values Work.gateCount = stepAvailable) : (emitStepPackedCopies tm).emitted values = List.flatMap CircuitCode.RawGate.encode (stepPackedCopies (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) stepAvailable (stepAtomKindAt tm (values Work.horizon)) (stepAtomEffectSelectedAt tm (values Work.horizon)) (effectCaseChoiceAt tm))

The complete delayed-copy phase emits exactly the canonical packed-copy suffix in global configuration-atom order.