Numeric transition-effect schedules -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.length_effectFormulaCaseBlock_internal (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (caseIndex : ℕ) (hcase : caseIndex < caseCount) : List.length (effectFormulaCaseBlock caseCount stateCount workCount T configBase choiceWire available selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt caseIndex) = effectFormulaSizeAt caseCount workCount T selectedAt choiceAt caseIndex

theorem Complexity.CircuitUnrolling.Serializer.length_effectFormulaCaseGates_internal (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (effectFormulaCaseGates caseCount stateCount workCount T configBase choiceWire available selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = prefixSize (effectFormulaSizeAt caseCount workCount T selectedAt choiceAt) caseCount

theorem Complexity.CircuitUnrolling.Serializer.length_effectFormulaSchedule_internal (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (effectFormulaSchedule caseCount stateCount workCount T configBase choiceWire available selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = effectFormulaScheduleSize caseCount workCount T selectedAt choiceAt

theorem Complexity.CircuitUnrolling.Serializer.getElem_effectFormulaSchedule_identity_internal (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : (effectFormulaSchedule caseCount stateCount workCount T configBase choiceWire available selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt)[prefixSize (effectFormulaSizeAt caseCount workCount T selectedAt choiceAt) caseCount] = CircuitCode.RawGate.constant 0 false

theorem Complexity.CircuitUnrolling.Serializer.getElem_effectFormulaSchedule_connector_internal (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (rank : Fin caseCount) : (effectFormulaSchedule caseCount stateCount workCount T configBase choiceWire available selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt)[prefixSize (effectFormulaSizeAt caseCount workCount T selectedAt choiceAt) caseCount + 1 + ↑rank] = indexedRightFoldConnector AndOrOp.or available caseCount (effectFormulaSizeAt caseCount workCount T selectedAt choiceAt) ↑rank

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_effectFormula_eq_schedule_internal {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (selects : TransitionEffect tm → Bool) : BoolFormula.compileRaw available (effectFormula tm T configBase choiceWire selects) = effectFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)