Verified direct packed-step generation

This module exposes the complete deterministic transition-layer generator. Its contracts cover the concrete machine, its clean entry domain, exact register effect, restored scratch convention, and byte-for-byte emitted packed transition fragment.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_sound {k : ℕ} (tm : TM k) : (emitStep tm).Sound

Complete deterministic packed-step generation is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_requires {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) : (emitStep tm).requires values

A clean work vector and positive tableau horizon satisfy the complete step generator's explicit domain.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_effect {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) : (emitStep tm).effect values = Function.update (Function.update (Function.update (Function.update values Work.available (values Work.available + stepScheduleSize (transitionCases tm.toNTM).length (Fintype.card tm.Q) k (values Work.horizon) (stepAtomKindAt tm.toNTM (values Work.horizon)) (stepAtomEffectSelectedAt tm.toNTM (values Work.horizon)) (effectCaseChoiceAt tm.toNTM))) Work.configBase (stepScheduleOutputBase (transitionCases tm.toNTM).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.available) (stepAtomKindAt tm.toNTM (values Work.horizon)) (stepAtomEffectSelectedAt tm.toNTM (values Work.horizon)) (effectCaseChoiceAt tm.toNTM))) Work.gateBound 0) Work.gateCount 0

The complete step advances the wire frontier by the exact numeric schedule size, records the packed successor base, and clears both gate bookkeeping registers.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_preserves_clean {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) : StepClean ((emitStep tm).effect values)

A complete step restores the reusable clean-entry convention.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_spaceBoundByWidth {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

A complete deterministic transition layer has an advertised all-prefix auxiliary-space bound controlled by one shared numeric width envelope.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_emitted {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) : (emitStep tm).emitted values = List.flatMap CircuitCode.RawGate.encode (stepFragment tm.toNTM (values Work.horizon) (values Work.configBase) 0 (values Work.available))

The emitted word is exactly the encoded canonical packed transition fragment, with deterministic choice wire zero.