Numeric schedules for next-configuration atoms

This module exposes a common natural-number interface for the five branches of nextFormula: state, head, immutable input cell, immutable writable marker, and positive writable cell. Each nontrivial branch reuses the corresponding public transition schedule.

Main results

• The branch length theorems give exact numeric gate counts.
• length_nextFormulaSchedule gives the exact count selected by an atom kind.
• The branch compilation theorems expose each literal schedule adapter.
• compileRaw_nextFormula_eq_schedule proves the common literal adapter.
• size_nextFormula_eq_scheduleSize identifies the formula size with that common numeric count.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_nextHaltedOrSchedule (haltWire available oldWire : ℕ) (nextSchedule : CircuitCode.RawCircuit) : List.length (nextHaltedOrSchedule haltWire available oldWire nextSchedule) = nextHaltedOrScheduleSize (List.length nextSchedule)

A one-gate old atom plus the halted-or wrapper contributes seven gates beyond the next-value child.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_nextStateFormulaSchedule (caseCount stateCount workCount T configBase choiceWire available stateIndex haltStateIndex : ℕ) (selectedAt choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (nextStateFormulaSchedule caseCount stateCount workCount T configBase choiceWire available stateIndex haltStateIndex selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = nextStateFormulaScheduleSize caseCount workCount T selectedAt choiceAt

Exact gate count of a state-atom schedule.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_nextHeadFormulaSchedule (caseCount stateCount workCount T configBase choiceWire available tapeIndex target haltStateIndex : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (nextHeadFormulaSchedule caseCount stateCount workCount T configBase choiceWire available tapeIndex target haltStateIndex selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = nextHeadFormulaScheduleSize caseCount workCount T selectedAt choiceAt

Exact gate count of a head-atom schedule.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_nextCellCopySchedule (stateCount tapeCount T configBase tapeIndex position symbolIndex : ℕ) : List.length (nextCellCopySchedule stateCount tapeCount T configBase tapeIndex position symbolIndex) = nextCellCopyScheduleSize

Immutable input and writable marker cells emit one copy gate.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_nextWrittenCellFormulaSchedule (caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex haltStateIndex : ℕ) (selectedAt choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (nextWrittenCellFormulaSchedule caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex haltStateIndex selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = nextWrittenCellFormulaScheduleSize caseCount workCount T selectedAt choiceAt

Exact gate count of a positive writable-cell schedule.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_nextFormulaSchedule (caseCount stateCount workCount T configBase choiceWire available atomKind stateIndex tapeIndex position symbolIndex haltStateIndex : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (nextFormulaSchedule caseCount stateCount workCount T configBase choiceWire available atomKind stateIndex tapeIndex position symbolIndex haltStateIndex selectedAt choiceAt caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = nextFormulaScheduleSize caseCount workCount T atomKind selectedAt choiceAt

Exact gate count selected by the common numeric atom-kind interface.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextStateFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (state : tm.Q) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire (ConfigAtom.state state)) = nextStateFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (stateIndex tm state) (nextHaltStateIndex tm) (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

Literal raw schedule for the state branch of nextFormula.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextHeadFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (tape : TapeSlot k) (target : Fin (T + 1)) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire (ConfigAtom.head tape target)) = nextHeadFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (↑tape.index) (↑target) (nextHaltStateIndex tm) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

Literal raw schedule for the head branch of nextFormula.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextInputCellFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (position : Fin (T + 2)) (symbol : Γ) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire (ConfigAtom.cell TapeSlot.input position symbol)) = nextCellCopySchedule (Fintype.card tm.Q) (k + 2) T configBase ↑TapeSlot.input.index ↑position ↑(symbolIndex symbol)

Literal one-gate raw schedule for an immutable input-cell atom.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextWritableMarkerFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (tape : WritableSlot k) (position : Fin (T + 2)) (symbol : Γ) (hposition : ↑position = 0) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire (ConfigAtom.cell tape.toTapeSlot position symbol)) = nextCellCopySchedule (Fintype.card tm.Q) (k + 2) T configBase ↑tape.toTapeSlot.index ↑position ↑(symbolIndex symbol)

Literal one-gate raw schedule for an immutable writable marker cell.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextWrittenCellFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (tape : WritableSlot k) (position : Fin (T + 2)) (symbol : Γ) (hposition : ↑position ≠ 0) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire (ConfigAtom.cell tape.toTapeSlot position symbol)) = nextWrittenCellFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (↑tape.toTapeSlot.index) (↑position) (↑(symbolIndex symbol)) (nextHaltStateIndex tm) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

Literal raw schedule for a positive writable-cell atom.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_nextFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (atom : ConfigAtom tm T) : BoolFormula.compileRaw available (nextFormula tm T configBase choiceWire atom) = nextFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (nextAtomKind atom) (nextAtomStateIndex tm atom) (nextAtomTapeIndex atom) (nextAtomPosition atom) (nextAtomSymbolIndex atom) (nextHaltStateIndex tm) (nextAtomEffectSelectedAt tm atom) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

Exact raw compilation order selected through the common numeric atom interface. Machine and atom data occur only in compile-time extractors; every argument of nextFormulaSchedule is natural-number or Boolean data.

theorem Complexity.CircuitUnrolling.Serializer.size_nextFormula_eq_scheduleSize {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) (atom : ConfigAtom tm T) : (nextFormula tm T configBase choiceWire atom).size = nextFormulaScheduleSize (transitionCases tm).length k T (nextAtomKind atom) (nextAtomEffectSelectedAt tm atom) (effectCaseChoiceAt tm)

The syntax-tree size of every next atom equals its selected numeric schedule count.