Verified direct moved-head formula generation

This module exposes the complete three-direction moved-head generator together with its clean entry domain, restored work-vector effect, and exact encoded numeric schedule.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula_sound {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : (emitMovedHeadFormula tm tape).Sound

Complete moved-head formula generation is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula_spaceBoundByWidth {k : ℕ} (tm : NTM k) (tape : TapeSlot k) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), MovedHeadFormulaClean (values inputLength)) (hhorizon : ∀ (inputLength : ℕ), 0 < values inputLength Work.horizon) (htarget : ∀ (inputLength : ℕ), values inputLength Work.position ≤ values inputLength Work.horizon) (havailable : ∀ (inputLength : ℕ), 1 ≤ values inputLength Work.available) (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 + 1 → values inputLength Work.available + movedHeadFormulaScheduleSize (transitionCases tm).length k (values inputLength Work.horizon) (movedHeadCaseSelectedAt tm tape) (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) + 2 * TM.binaryPolynomialValueCap predecessorHeadSchedulePolynomial (values inputLength Work.horizon) + 2 * (values inputLength Work.horizon + 2) + values inputLength Work.horizon ≤ width inputLength) : (emitMovedHeadFormula tm tape).SpaceBoundByWidthAt initialSpace values width

Complete moved-head emission has an all-prefix width certificate under one bounded-selector envelope. The full schedule covers every member frontier; the remaining visible terms cover nested case references, predecessor-head references and controller slack, and the conjunction's polynomial evaluator.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula_requires {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) (havailable : 1 ≤ values Work.available) : (emitMovedHeadFormula tm tape).requires values

Clean owned scratch, a positive horizon, an in-range target, and a valid wire frontier suffice for complete moved-head formula generation.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula_effect {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) (havailable : 1 ≤ values Work.available) : (emitMovedHeadFormula tm tape).effect values = Function.update values Work.available (values Work.available + movedHeadFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm))

Moved-head generation restores every owned register and advances only the wire frontier by the exact numeric schedule size.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula_emitted {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) (havailable : 1 ≤ values Work.available) : (emitMovedHeadFormula tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (movedHeadFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (↑tape.index) (values Work.position) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

The emitted word is literally the canonical numeric moved-head schedule, including all three direction members, the false identity, and reverse fold.