Verified direct next-atom generation

This module exposes exact contracts for the four executable branches used by the packed-step generator: state, head, immutable-cell copy, and writable-cell update. The step dispatcher uses the update routine only at positive positions; its numeric schedule contract itself remains valid at every in-range position. Input cells and writable marker cells share the same copy routine because their canonical raw schedules are literally identical.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy_sound (stateCount tapeCount tapeIndex symbolIndex : ℕ) : (emitNextCellCopy stateCount tapeCount tapeIndex symbolIndex).Sound

One immutable-cell copy is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy_requires (stateCount tapeCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hemit : values Work.emitCounter = 0) : (emitNextCellCopy stateCount tapeCount tapeIndex symbolIndex).requires values

The arithmetic and emission scratch required by an immutable-cell copy.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy_spaceBoundByWidth (stateCount tapeCount tapeIndex symbolIndex : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength : ℕ), transitionCellRef stateCount tapeCount (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex (values inputLength Work.position) symbolIndex + (tapeIndex * (values inputLength Work.horizon + 2) + values inputLength Work.position) + (values inputLength Work.horizon + 2) + tapeCount + tapeIndex + 4 ≤ width inputLength) : (emitNextCellCopy stateCount tapeCount tapeIndex symbolIndex).SpaceBoundByWidthAt initialSpace values width

An immutable-cell copy has an all-prefix width certificate when its fixed selectors and the complete absolute-reference arithmetic fit one width.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy_effect (stateCount tapeCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) (htape : values Work.tapeIndex = 0) (hsymbol : values Work.symbolIndex = 0) (htemporary₀ : values Work.temporary₀ = 0) (htemporary₁ : values Work.temporary₁ = 0) (htemporary₂ : values Work.temporary₂ = 0) (hreference : values Work.reference₀ = 0) : (emitNextCellCopy stateCount tapeCount tapeIndex symbolIndex).effect values = Function.update values Work.available (values Work.available + 1)

An immutable-cell copy restores its scratch and advances the frontier by exactly one gate.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextCellCopy_emitted (stateCount tapeCount tapeIndex symbolIndex : ℕ) (values : BinaryValues WorkCount) : (emitNextCellCopy stateCount tapeCount tapeIndex symbolIndex).emitted values = List.flatMap CircuitCode.RawGate.encode (nextCellCopySchedule stateCount tapeCount (values Work.horizon) (values Work.configBase) tapeIndex (values Work.position) symbolIndex)

An immutable input or writable marker cell emits its literal canonical one-gate copy schedule.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextStateFormula_sound {k : ℕ} (tm : NTM k) (state : tm.Q) : (emitNextStateFormula tm state).Sound

Complete state-atom next-formula generation is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextStateFormula_requires {k : ℕ} (tm : NTM k) (state : tm.Q) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitNextStateFormula tm state).requires values

Clean case-formula scratch suffices for a complete state-atom formula.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextStateFormula_spaceBoundByWidth {k : ℕ} (tm : NTM k) (state : tm.Q) {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 + nextStateFormulaScheduleSize (transitionCases tm).length k (values inputLength Work.horizon) (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (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 + 2 * TM.binaryPolynomialValueCap (stateNextChildPolynomial tm state) (values inputLength Work.horizon) ≤ width inputLength) : (emitNextStateFormula tm state).SpaceBoundByWidthAt initialSpace values width

Complete state-atom generation has an all-prefix width certificate under one envelope covering its frontier, nested selected-effect references, and the fixed child-size polynomial evaluator.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextStateFormula_effect {k : ℕ} (tm : NTM k) (state : tm.Q) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitNextStateFormula tm state).effect values = Function.update values Work.available (values Work.available + nextStateFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm))

State-atom generation restores every owned register and advances only the wire frontier by its exact schedule size.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextStateFormula_emitted {k : ℕ} (tm : NTM k) (state : tm.Q) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitNextStateFormula tm state).emitted values = List.flatMap CircuitCode.RawGate.encode (nextStateFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (stateIndex tm state) (stateIndex tm tm.qhalt) (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

State-atom generation emits the canonical numeric halted-or schedule byte for byte.

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

Complete head-atom next-formula generation is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextHeadFormula_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) : (emitNextHeadFormula tm tape).requires values

Clean moved-head scratch, a positive horizon, and an in-range target suffice for a complete head-atom formula.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextHeadFormula_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) (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 + nextHeadFormulaScheduleSize (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 + 2 * TM.binaryPolynomialValueCap (headNextChildPolynomial tm tape) (values inputLength Work.horizon) ≤ width inputLength) : (emitNextHeadFormula tm tape).SpaceBoundByWidthAt initialSpace values width

Complete head-atom generation has an all-prefix width certificate under one envelope covering the moved-head child, predecessor arithmetic, both polynomial evaluators, and every absolute configuration reference.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextHeadFormula_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) : (emitNextHeadFormula tm tape).effect values = Function.update values Work.available (values Work.available + nextHeadFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm))

Head-atom generation restores every owned register and advances only the wire frontier by its exact schedule size.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextHeadFormula_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) : (emitNextHeadFormula tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (nextHeadFormulaSchedule (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) (stateIndex tm tm.qhalt) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

Head-atom generation emits the canonical numeric moved-head wrapper schedule byte for byte.

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

Complete positive writable-cell next-formula generation is sound.

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

Clean writable-cell scratch and an in-range position suffice for a complete positive writable-cell formula.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextWrittenCellFormula_spaceBoundByWidth {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), WrittenCellFormulaClean (values inputLength)) (hposition : ∀ (inputLength : ℕ), values inputLength Work.position ≤ values inputLength Work.horizon + 1) (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 + nextWrittenCellFormulaScheduleSize (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 + 2 * TM.binaryPolynomialValueCap (writtenNextChildPolynomial tm tape symbol) (values inputLength Work.horizon) ≤ width inputLength) : (emitNextWrittenCellFormula tm tape symbol).SpaceBoundByWidthAt initialSpace values width

Complete writable-cell generation has an all-prefix width certificate under one envelope covering its halted wrapper, nested selected-write child, absolute references, and child-size polynomial evaluator.

@[simp]

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

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

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitNextWrittenCellFormula_emitted {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : WrittenCellFormulaClean values) (hposition : values Work.position ≤ values Work.horizon + 1) : (emitNextWrittenCellFormula tm tape symbol).emitted values = List.flatMap CircuitCode.RawGate.encode (nextWrittenCellFormulaSchedule (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)) (stateIndex tm tm.qhalt) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

Writable-cell generation emits the canonical numeric halted-or schedule byte for byte.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.stateNextChildPolynomial_eval {k : ℕ} (tm : NTM k) (state : tm.Q) (T : ℕ) : Polynomial.eval T (stateNextChildPolynomial tm state) = effectFormulaScheduleSize (transitionCases tm).length k T (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm)

Exact selected-effect child size for a state atom.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.stateNextFormulaPolynomial_eval {k : ℕ} (tm : NTM k) (state : tm.Q) (T : ℕ) : Polynomial.eval T (stateNextFormulaPolynomial tm state) = nextStateFormulaScheduleSize (transitionCases tm).length k T (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm)

Exact complete state-atom schedule size.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.headNextChildPolynomial_eval {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (T : ℕ) : Polynomial.eval T (headNextChildPolynomial tm tape) = movedHeadFormulaScheduleSize (transitionCases tm).length k T (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm)

Exact moved-head child size for a head atom.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.headNextFormulaPolynomial_eval {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (T : ℕ) : Polynomial.eval T (headNextFormulaPolynomial tm tape) = nextHeadFormulaScheduleSize (transitionCases tm).length k T (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm)

Exact complete head-atom schedule size.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.writtenNextChildPolynomial_eval {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (T : ℕ) : Polynomial.eval T (writtenNextChildPolynomial tm tape symbol) = writtenCellScheduleSize (transitionCases tm).length k T (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm)

Exact written-cell child size for a writable-cell atom.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.writtenNextFormulaPolynomial_eval {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (T : ℕ) : Polynomial.eval T (writtenNextFormulaPolynomial tm tape symbol) = nextWrittenCellFormulaScheduleSize (transitionCases tm).length k T (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm)

Exact complete writable-cell schedule size.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.stateNextFormulaPolynomial_eval_pos {k : ℕ} (tm : NTM k) (state : tm.Q) (T : ℕ) : 0 < Polynomial.eval T (stateNextFormulaPolynomial tm state)

A complete state-atom formula always emits at least one gate.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.headNextFormulaPolynomial_eval_pos {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (T : ℕ) : 0 < Polynomial.eval T (headNextFormulaPolynomial tm tape)

A complete head-atom formula always emits at least one gate.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.writtenNextFormulaPolynomial_eval_pos {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (T : ℕ) : 0 < Polynomial.eval T (writtenNextFormulaPolynomial tm tape symbol)

A complete writable-cell formula always emits at least one gate.