Direct-unrolling finalization generator

This module exposes the verified acceptance, dead-padding, and terminal-copy phase of the executable direct-unrolling serializer. Padding is driven by the binary available counter and the precomputed closed frontier, so the routine uses logarithmic-width work values and performs no preliminary counting pass.

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

Preparing the two numeric acceptance references is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceReferences_requires {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) : (prepareAcceptanceReferences tm).requires values

The arithmetic preparation domain follows from its two reusable zero counters.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceReferences_effect {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (prepareAcceptanceReferences tm).effect values = acceptanceReferenceValues tm values

Exact pure endpoint of acceptance-reference preparation.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceReferences_emitted {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (prepareAcceptanceReferences tm).emitted values = []

Reference preparation emits no code bits.

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

Saving and emitting the original acceptance gate is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitAcceptance_requires {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) (hcopy : values Work.copyCounter = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) : (emitAcceptance tm).requires values

The acceptance phase's reusable-counter domain.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitAcceptance_effect {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (emitAcceptance tm).effect values = afterAcceptanceValues tm values

Exact pure endpoint after the original acceptance gate.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitAcceptance_emitted {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (emitAcceptance tm).emitted values = (currentAcceptanceGate tm values).encode

The acceptance phase emits exactly the numeric acceptance gate.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPadding_sound : emitPadding.Sound

The dead-gate loop is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPadding_requires (values : BinaryValues WorkCount) (hle : values Work.available ≤ values Work.frontier) (hemit : values Work.emitCounter = 0) : emitPadding.requires values

The dead-gate loop's controller and emission precondition.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPadding_spaceBoundByWidth {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hfrontier : ∀ (inputLength : ℕ), values inputLength Work.frontier ≤ width inputLength) (hreference : ∀ (inputLength : ℕ), values inputLength Work.reference₀ ≤ width inputLength) : emitPadding.SpaceBoundByWidthAt initialSpace values width

Padding retains a fixed-width pointwise space certificate whenever its closed frontier and preserved zero reference fit that width. The number of emitted dead gates does not contribute additively to auxiliary space.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPadding_emitted (values : BinaryValues WorkCount) (hzero : values Work.reference₀ = 0) : emitPadding.emitted values = List.flatMap CircuitCode.RawGate.encode (List.replicate (values Work.frontier - values Work.available) (CircuitCode.RawGate.constant 0 false))

From a zero reference, padding emits exactly the closed-frontier shortfall as constant-false raw gates.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTerminalCopy_sound : emitTerminalCopy.Sound

The terminal acceptance-wire copy is sound.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTerminalCopy_emitted (values : BinaryValues WorkCount) : emitTerminalCopy.emitted values = (CircuitCode.RawGate.copy (values Work.savedOutput)).encode

Exact terminal copy emitted from the saved output reference.

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

The complete finalization phase is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_requires {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) (hcopy : values Work.copyCounter = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hle : values Work.available + 1 ≤ values Work.frontier) : (finalization tm).requires values

Finalization is available whenever all reusable counters are zero and the acceptance gate still fits below the closed padding frontier.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_spaceBoundByPolynomial {k : ℕ} (tm : TM k) (p : Polynomial ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ Polynomial.eval inputLength p) : ∃ (width : Polynomial ℕ), (finalization tm).SpaceBoundByWidthAt initialSpace values fun (x : ℕ) => Polynomial.eval x width

If every incoming work value is bounded by one fixed polynomial, then the full acceptance, padding, terminal-copy, and cleanup phase has a pointwise polynomial-width auxiliary-space certificate.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_space_bigO_log {k : ℕ} (tm : TM k) (p : Polynomial ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} (hinitial : BigO initialSpace fun (inputLength : ℕ) => Nat.log 2 inputLength) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ Polynomial.eval inputLength p) : (finalization tm).SpaceBoundInLogAt initialSpace values

Polynomially bounded incoming work values make the complete finalization phase logarithmic-space, provided the incoming auxiliary-space budget is already logarithmic.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_emitted {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (finalization tm).emitted values = (currentAcceptanceGate tm values).encode ++ List.flatMap CircuitCode.RawGate.encode (List.replicate (values Work.frontier - (values Work.available + 1)) (CircuitCode.RawGate.constant 0 false)) ++ (CircuitCode.RawGate.copy (values Work.available)).encode

Exact acceptance, padding, and terminal-copy word from an arbitrary pure entry vector.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_emitted_eq_numericSchedule {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (n originalRawGateCount closedBound T finalConfigBase : ℕ) (hn : 0 < n) (havailable : values Work.available = n + originalRawGateCount - 1) (hfrontier : values Work.frontier = n + closedBound) (hhorizon : values Work.horizon = T) (hconfigBase : values Work.configBase = finalConfigBase) : (finalization tm).emitted values = List.flatMap CircuitCode.RawGate.encode ([numericAcceptanceGate (Fintype.card tm.Q) (stateIndex tm.toNTM tm.qhalt) (k + 2) T finalConfigBase] ++ directFinalizationSuffix n originalRawGateCount closedBound)

Under the numeric tableau endpoint equations, finalization emits exactly the serializer's acceptance gate and padded suffix.