Direct-unrolling transition-effect generator

Exact contracts for the generated disjunction over a machine's finite transition table.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula_sound {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) : (emitEffectFormula tm selects).Sound

Complete transition-effect emission is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula_spaceBoundByWidth {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), CaseFormulaClean (values inputLength)) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength stateIndex tapeIndex symbolIndex position : ℕ), stateIndex < Fintype.card tm.Q → tapeIndex ≤ k + 1 → symbolIndex < 4 → position ≤ values inputLength Work.horizon → values inputLength Work.available + effectFormulaScheduleSize (transitionCases tm).length k (values inputLength Work.horizon) (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm) + transitionStateRef (values inputLength Work.configBase) stateIndex + (transitionHeadRef (Fintype.card tm.Q) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position + tapeIndex + values inputLength Work.horizon + 1) + (transitionCellRef (Fintype.card tm.Q) (k + 2) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position symbolIndex + (tapeIndex * (values inputLength Work.horizon + 2) + position) + (values inputLength Work.horizon + 2) + (k + 2) + tapeIndex + 4) + caseReadSize (values inputLength Work.horizon) + values inputLength Work.horizon ≤ width inputLength) : (emitEffectFormula tm selects).SpaceBoundByWidthAt initialSpace values width

Complete transition-effect emission has an all-prefix width certificate under one global bounded-selector envelope. The cap covers the complete wire frontier together with every state, head, cell, and read-size intermediate that any machine-selected case can use.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula_requires {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitEffectFormula tm selects).requires values

Clean scratch together with a positive wire frontier suffices for every leaf routine in complete transition-effect emission.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula_effect {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitEffectFormula tm selects).effect values = Function.update values Work.available (values Work.available + effectFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm))

Complete transition-effect emission restores all owned scratch and advances only the wire frontier by the exact numeric schedule size.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula_emitted {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitEffectFormula tm selects).emitted values = List.flatMap CircuitCode.RawGate.encode (effectFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

Complete transition-effect emission is literally the canonical numeric raw-gate schedule, including its false identity and reverse connector suffix.