Numeric transition-case schedules

This module exposes the exact natural-index schedule for one fixed local transition case. Its run-time parameters are natural numbers and one Boolean choice value; machine states, tape slots, symbols, and formula syntax occur only in the final compilation adapter.

Main results

• length_caseFormulaSchedule gives the exact gate count.
• The getElem_caseFormulaSchedule_* theorems identify every numeric phase.
• compileRaw_caseFormula_eq_schedule identifies the complete raw stream.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_caseChoiceLiteralSchedule (available choiceWire : ℕ) (choiceValue : Bool) : List.length (caseChoiceLiteralSchedule available choiceWire choiceValue) = caseChoiceLiteralSize choiceValue

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_caseWorkReadGates (stateCount workCount T configBase available : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) : List.length (caseWorkReadGates stateCount workCount T configBase available choiceValue workSymbolAt) = workCount * caseReadSize T

theorem Complexity.CircuitUnrolling.Serializer.getElem_caseWorkReadGates (stateCount workCount T configBase available : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) (workIndex : Fin workCount) (offset : Fin (caseReadSize T)) : (caseWorkReadGates stateCount workCount T configBase available choiceValue workSymbolAt)[↑workIndex * caseReadSize T + ↑offset] = (readFormulaSchedule stateCount (workCount + 2) T configBase (caseWorkReadAvailable T available (↑workIndex) choiceValue) (↑workIndex + 1) (workSymbolAt ↑workIndex))[↑offset]

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_caseFormulaMemberGates (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) : List.length (caseFormulaMemberGates stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolAt) = caseFormulaMembersSize workCount T choiceValue

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_caseFormulaSchedule (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) : List.length (caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolAt) = caseFormulaScheduleSize workCount T choiceValue

theorem Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_choice (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) (offset : Fin (caseChoiceLiteralSize choiceValue)) : (caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolAt)[↑offset] = (caseChoiceLiteralSchedule available choiceWire choiceValue)[↑offset]

theorem Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_state (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) : (caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolAt)[caseChoiceLiteralSize choiceValue] = CircuitCode.RawGate.copy (transitionStateRef configBase stateIndex)

theorem Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_inputRead (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) (offset : Fin (caseReadSize T)) : (caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolAt)[caseChoiceLiteralSize choiceValue + 1 + ↑offset] = (readFormulaSchedule stateCount (workCount + 2) T configBase (caseInputReadAvailable available choiceValue) 0 inputSymbolIndex)[↑offset]

theorem Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_workRead (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) (workIndex : Fin workCount) (offset : Fin (caseReadSize T)) : (caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolAt)[caseChoiceLiteralSize choiceValue + 1 + caseReadSize T + ↑workIndex * caseReadSize T + ↑offset] = (readFormulaSchedule stateCount (workCount + 2) T configBase (caseWorkReadAvailable T available (↑workIndex) choiceValue) (↑workIndex + 1) (workSymbolAt ↑workIndex))[↑offset]

theorem Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_outputRead (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) (offset : Fin (caseReadSize T)) : (caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolAt)[caseChoiceLiteralSize choiceValue + 1 + (workCount + 1) * caseReadSize T + ↑offset] = (readFormulaSchedule stateCount (workCount + 2) T configBase (caseOutputReadAvailable workCount T available choiceValue) (workCount + 1) outputSymbolIndex)[↑offset]

theorem Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_identity (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) : (caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolAt)[caseFormulaMembersSize workCount T choiceValue] = CircuitCode.RawGate.constant 0 true

theorem Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_connector (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) (rank : Fin (caseFormulaMemberCount workCount)) : (caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolAt)[caseFormulaMembersSize workCount T choiceValue + 1 + ↑rank] = indexedRightFoldConnector AndOrOp.and available (caseFormulaMemberCount workCount) (caseFormulaSizeAt workCount T choiceValue) ↑rank

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_caseFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (view : TransitionCase tm) : BoolFormula.compileRaw available (caseFormula tm T configBase choiceWire view) = caseFormulaSchedule (Fintype.card tm.Q) k T configBase choiceWire available (stateIndex tm view.state) (↑(symbolIndex view.inputRead)) (↑(symbolIndex view.outputRead)) view.choice fun (index : ℕ) => if hindex : index < k then ↑(symbolIndex (view.workRead ⟨index, hindex⟩)) else 0

Exact raw compilation order of one fixed local transition case.