Numeric written-cell schedules -- proof internals #
theorem
Complexity.CircuitUnrolling.Serializer.length_writtenCellSuffixGates_internal
(stateCount tapeCount T configBase available tapeIndex position symbolIndex effectSize : ℕ)
:
List.length
(writtenCellSuffixGates stateCount tapeCount T configBase available tapeIndex position symbolIndex effectSize) = 6
theorem
Complexity.CircuitUnrolling.Serializer.getElem_writtenCellSuffixGates_internal
(stateCount tapeCount T configBase available tapeIndex position symbolIndex effectSize : ℕ)
(phase : Fin 6)
:
(writtenCellSuffixGates stateCount tapeCount T configBase available tapeIndex position symbolIndex effectSize)[↑phase] = writtenCellSuffixGate stateCount tapeCount T configBase available tapeIndex position symbolIndex effectSize ↑phase
theorem
Complexity.CircuitUnrolling.Serializer.length_writtenCellSchedule_internal
(caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex : ℕ)
(selectedAt choiceAt : ℕ → Bool)
(stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ)
(workSymbolIndexAt : ℕ → ℕ → ℕ)
:
List.length
(writtenCellSchedule caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex
selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = writtenCellScheduleSize caseCount workCount T selectedAt choiceAt
theorem
Complexity.CircuitUnrolling.Serializer.getElem_writtenCellSchedule_head_internal
(caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex : ℕ)
(selectedAt choiceAt : ℕ → Bool)
(stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ)
(workSymbolIndexAt : ℕ → ℕ → ℕ)
:
(writtenCellSchedule caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex
selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt)[0] = headAtCellFormulaGate stateCount T configBase tapeIndex position
theorem
Complexity.CircuitUnrolling.Serializer.getElem_writtenCellSchedule_effect_internal
(caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex : ℕ)
(selectedAt choiceAt : ℕ → Bool)
(stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ)
(workSymbolIndexAt : ℕ → ℕ → ℕ)
(offset : Fin (writtenCellEffectSize caseCount workCount T selectedAt choiceAt))
:
(writtenCellSchedule caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex
selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt)[↑offset + 1] = (effectFormulaSchedule caseCount stateCount workCount T configBase choiceWire (available + 1) selectedAt choiceAt
stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt)[↑offset]
theorem
Complexity.CircuitUnrolling.Serializer.getElem_writtenCellSchedule_suffix_internal
(caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex : ℕ)
(selectedAt choiceAt : ℕ → Bool)
(stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ)
(workSymbolIndexAt : ℕ → ℕ → ℕ)
(phase : Fin 6)
:
(writtenCellSchedule caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex
selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt
workSymbolIndexAt)[writtenCellEffectSize caseCount workCount T selectedAt choiceAt + 1 + ↑phase] = writtenCellSuffixGate stateCount (workCount + 2) T configBase available tapeIndex position symbolIndex
(writtenCellEffectSize caseCount workCount T selectedAt choiceAt) ↑phase
theorem
Complexity.CircuitUnrolling.Serializer.compileRaw_writtenCellFormula_eq_schedule_internal
{k : ℕ}
(tm : NTM k)
(T configBase choiceWire available : ℕ)
(tape : WritableSlot k)
(position : Fin (T + 2))
(symbol : Γ)
:
BoolFormula.compileRaw available (writtenCellFormula tm T configBase choiceWire tape position symbol) = writtenCellSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available
(↑tape.toTapeSlot.index) (↑position) (↑(symbolIndex symbol)) (writtenCellEffectSelectedAt tm tape symbol)
(effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm)
(effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)