Verified direct written-cell formula generation

This module exposes the complete positive-cell formula generator together with its clean entry domain, restored work-vector effect, and exact encoded numeric schedule.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula_sound {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) : (emitWrittenCellFormula tm tape symbol).Sound

Complete written-cell formula generation is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula_spaceBoundByWidth {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), WrittenCellFormulaClean (values inputLength)) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hposition : ∀ (inputLength : ℕ), values inputLength Work.position ≤ values inputLength Work.horizon + 1) (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 + writtenCellScheduleSize (transitionCases tm).length k (values inputLength Work.horizon) (writtenCellEffectSelectedAt tm tape symbol) (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) : (emitWrittenCellFormula tm tape symbol).SpaceBoundByWidthAt initialSpace values width

Complete written-cell 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 used by the nested effect and fixed wrapper phases.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula_requires {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : WrittenCellFormulaClean values) (hposition : values Work.position ≤ values Work.horizon + 1) : (emitWrittenCellFormula tm tape symbol).requires values

Clean owned scratch and an in-range positive-cell position suffice for complete written-cell formula generation.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula_effect {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : WrittenCellFormulaClean values) : (emitWrittenCellFormula tm tape symbol).effect values = Function.update values Work.available (values Work.available + writtenCellScheduleSize (transitionCases tm).length k (values Work.horizon) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm))

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

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula_emitted {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : WrittenCellFormulaClean values) (hposition : values Work.position ≤ values Work.horizon + 1) : (emitWrittenCellFormula tm tape symbol).emitted values = List.flatMap CircuitCode.RawGate.encode (writtenCellSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (↑tape.toTapeSlot.index) (values Work.position) (↑(symbolIndex symbol)) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

The emitted word is literally the canonical numeric written-cell schedule, including both head tests, the selected-write effect, and the preservation branch.