Numeric moved-head schedules -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_mono_movedHead_internal (sizeAt : ℕ → ℕ) {first second : ℕ} (hbound : first ≤ second) : prefixSize sizeAt first ≤ prefixSize sizeAt second

theorem Complexity.CircuitUnrolling.Serializer.length_movedHeadMemberBlock_internal (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (directionCode : ℕ) (hdirection : directionCode < movedHeadDirectionCount) : List.length (movedHeadMemberBlock caseCount stateCount workCount T configBase choiceWire available tapeIndex target selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt directionCode) = movedHeadMemberSizeAt caseCount workCount T selectedAt choiceAt directionCode

theorem Complexity.CircuitUnrolling.Serializer.length_movedHeadMemberGates_internal (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (movedHeadMemberGates caseCount stateCount workCount T configBase choiceWire available tapeIndex target selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = prefixSize (movedHeadMemberSizeAt caseCount workCount T selectedAt choiceAt) movedHeadDirectionCount

theorem Complexity.CircuitUnrolling.Serializer.getElem_movedHeadMemberGates_internal (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (directionCode offset : ℕ) (hdirection : directionCode < movedHeadDirectionCount) (hoffset : offset < movedHeadMemberSizeAt caseCount workCount T selectedAt choiceAt directionCode) : (movedHeadMemberGates caseCount stateCount workCount T configBase choiceWire available tapeIndex target selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt)[prefixSize (movedHeadMemberSizeAt caseCount workCount T selectedAt choiceAt) directionCode + offset] = (movedHeadMemberBlock caseCount stateCount workCount T configBase choiceWire available tapeIndex target selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt directionCode)[offset]

theorem Complexity.CircuitUnrolling.Serializer.getElem_movedHeadMemberBlock_effect_internal (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (directionCode offset : ℕ) (hdirection : directionCode < movedHeadDirectionCount) (hoffset : offset < movedHeadEffectSizeAt caseCount workCount T selectedAt choiceAt directionCode) : (movedHeadMemberBlock caseCount stateCount workCount T configBase choiceWire available tapeIndex target selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt directionCode)[offset] = (effectFormulaSchedule caseCount stateCount workCount T configBase choiceWire (movedHeadMemberAvailable caseCount workCount T available selectedAt choiceAt directionCode) (selectedAt directionCode) choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt)[offset]

theorem Complexity.CircuitUnrolling.Serializer.getElem_movedHeadMemberBlock_predecessor_internal (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (directionCode offset : ℕ) (hdirection : directionCode < movedHeadDirectionCount) (hoffset : offset < movedHeadPredecessorSize T) : (movedHeadMemberBlock caseCount stateCount workCount T configBase choiceWire available tapeIndex target selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt directionCode)[movedHeadEffectSizeAt caseCount workCount T selectedAt choiceAt directionCode + offset] = (predecessorHeadFormulaSchedule stateCount T configBase (movedHeadPredecessorAvailable caseCount workCount T available selectedAt choiceAt directionCode) tapeIndex target directionCode)[offset]

theorem Complexity.CircuitUnrolling.Serializer.getElem_movedHeadMemberBlock_conjunction_internal (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (directionCode : ℕ) (hdirection : directionCode < movedHeadDirectionCount) : (movedHeadMemberBlock caseCount stateCount workCount T configBase choiceWire available tapeIndex target selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt directionCode)[movedHeadEffectSizeAt caseCount workCount T selectedAt choiceAt directionCode + movedHeadPredecessorSize T] = movedHeadConjunctionGate caseCount workCount T available selectedAt choiceAt directionCode

theorem Complexity.CircuitUnrolling.Serializer.length_movedHeadFormulaSchedule_internal (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (movedHeadFormulaSchedule caseCount stateCount workCount T configBase choiceWire available tapeIndex target selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = movedHeadFormulaScheduleSize caseCount workCount T selectedAt choiceAt

theorem Complexity.CircuitUnrolling.Serializer.getElem_movedHeadFormulaSchedule_identity_internal (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : (movedHeadFormulaSchedule caseCount stateCount workCount T configBase choiceWire available tapeIndex target selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt)[prefixSize (movedHeadMemberSizeAt caseCount workCount T selectedAt choiceAt) movedHeadDirectionCount] = CircuitCode.RawGate.constant 0 false

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

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