Numeric schedules for written-cell formulas

This module exposes the numeric schedule for writtenCellFormula. One head-at-cell gate precedes the reused transition-effect schedule, and a fixed six-gate suffix combines the selected write with the old cell value.

Main results

• length_writtenCellSchedule gives the exact gate count.
• getElem_writtenCellSchedule_head, getElem_writtenCellSchedule_effect, and getElem_writtenCellSchedule_suffix identify the three schedule phases.
• compileRaw_writtenCellFormula_eq_schedule proves literal raw-list equality.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_writtenCellSuffixGates (stateCount tapeCount T configBase available tapeIndex position symbolIndex effectSize : ℕ) : List.length (writtenCellSuffixGates stateCount tapeCount T configBase available tapeIndex position symbolIndex effectSize) = 6

The fixed suffix contains exactly six gates.

theorem Complexity.CircuitUnrolling.Serializer.getElem_writtenCellSuffixGates (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

A bounded natural phase selects the corresponding fixed suffix gate.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_writtenCellSchedule (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

The complete written-cell schedule has the advertised numeric size.

theorem Complexity.CircuitUnrolling.Serializer.getElem_writtenCellSchedule_head (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

Phase zero is the initial head-at-cell test.

theorem Complexity.CircuitUnrolling.Serializer.getElem_writtenCellSchedule_effect (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]

The block after the head test is exactly the reused effect schedule.

theorem Complexity.CircuitUnrolling.Serializer.getElem_writtenCellSchedule_suffix (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

The final six entries are selected by an increasing natural phase code.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_writtenCellFormula_eq_schedule {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)

Exact raw compilation order of a written-cell formula. The dynamic schedule inputs are natural numbers or Booleans; tm, tape, and symbol determine only the fixed selection oracle.