Numeric schedules for one packed transition step

This module exposes the canonical whole-step schedule. It streams one numeric nextFormula block per configuration atom in explicit wire order, then emits one packed-output copy per atom in that same order.

Main results

• length_stepFormulaBlock and length_stepFormulaGates expose exact formula block and prefix sizes.
• getElem_stepPackedCopies identifies every delayed output reference.
• length_stepSchedule gives the exact whole-step gate count.
• stepFragment_eq_stepSchedule proves literal equality with the existing packed transition fragment.
• stepOutputBase_eq_stepScheduleOutputBase and stepScheduleOutputRef_configIndex connect numeric output references to the public successor-configuration layout.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_stepFormulaBlock (caseCount stateCount workCount T configBase choiceWire available haltStateIndex : ℕ) (kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (atomIndex : ℕ) (hindex : atomIndex < stepAtomCount stateCount workCount T) : List.length (stepFormulaBlock caseCount stateCount workCount T configBase choiceWire available haltStateIndex kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt atomIndex) = stepFormulaSizeAt caseCount stateCount workCount T kindAt selectedAt choiceAt atomIndex

An in-range atom block has exactly its advertised numeric size.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_stepFormulaGates (caseCount stateCount workCount T configBase choiceWire available haltStateIndex : ℕ) (kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (stepFormulaGates caseCount stateCount workCount T configBase choiceWire available haltStateIndex kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = prefixSize (stepFormulaSizeAt caseCount stateCount workCount T kindAt selectedAt choiceAt) (stepAtomCount stateCount workCount T)

The complete forward formula phase is the prefix sum of all atom sizes.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_stepPackedCopies (caseCount stateCount workCount T available : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) : List.length (stepPackedCopies caseCount stateCount workCount T available kindAt selectedAt choiceAt) = stepAtomCount stateCount workCount T

The packed suffix contains exactly one copy gate per atom.

theorem Complexity.CircuitUnrolling.Serializer.getElem_stepPackedCopies (caseCount stateCount workCount T available : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (atomIndex : Fin (stepAtomCount stateCount workCount T)) : (stepPackedCopies caseCount stateCount workCount T available kindAt selectedAt choiceAt)[↑atomIndex] = stepPackedCopyGate caseCount stateCount workCount T available kindAt selectedAt choiceAt ↑atomIndex

Packed-copy index recovers the formula-output reference computed by the numeric prefix oracle.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_stepSchedule (caseCount stateCount workCount T configBase choiceWire available haltStateIndex : ℕ) (kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (stepSchedule caseCount stateCount workCount T configBase choiceWire available haltStateIndex kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = stepScheduleSize caseCount stateCount workCount T kindAt selectedAt choiceAt

Exact gate count of the complete numeric packed step.

theorem Complexity.CircuitUnrolling.Serializer.stepFragment_eq_stepSchedule {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : stepFragment tm T configBase choiceWire available = stepSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (nextHaltStateIndex tm) (stepAtomKindAt tm T) (stepAtomStateIndexAt tm T) (stepAtomTapeIndexAt tm T) (stepAtomPositionAt tm T) (stepAtomSymbolIndexAt tm T) (stepAtomEffectSelectedAt tm T) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

Literal equality between the existing packed transition fragment and the canonical numeric whole-step schedule.

theorem Complexity.CircuitUnrolling.Serializer.stepFragmentSize_eq_stepScheduleSize {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) : stepFragmentSize tm T configBase choiceWire = stepScheduleSize (transitionCases tm).length (Fintype.card tm.Q) k T (stepAtomKindAt tm T) (stepAtomEffectSelectedAt tm T) (effectCaseChoiceAt tm)

The existing packed fragment size is exactly the numeric schedule count.

theorem Complexity.CircuitUnrolling.Serializer.stepOutputBase_eq_stepScheduleOutputBase {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : stepOutputBase tm T configBase choiceWire available = stepScheduleOutputBase (transitionCases tm).length (Fintype.card tm.Q) k T available (stepAtomKindAt tm T) (stepAtomEffectSelectedAt tm T) (effectCaseChoiceAt tm)

The numeric prefix total is exactly the existing packed successor base.

theorem Complexity.CircuitUnrolling.Serializer.stepScheduleOutputRef_configIndex {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (atom : ConfigAtom tm T) : stepScheduleOutputRef (transitionCases tm).length (Fintype.card tm.Q) k T available (stepAtomKindAt tm T) (stepAtomEffectSelectedAt tm T) (effectCaseChoiceAt tm) (configIndex tm T atom) = configWire tm T (stepOutputBase tm T configBase choiceWire available) atom

A numeric packed-output reference at an atom's explicit index is exactly its successor-configuration wire.