Numeric moved-head schedules

This module exposes a natural-index stream for movedHeadFormula. The three direction members are compiled forward; each contains an effect phase, a predecessor-head phase, and one conjunction gate. A false identity and three reverse disjunction connectors complete the stream.

Main results

• length_movedHeadFormulaSchedule gives the exact total gate count.
• The member and child-phase lookup theorems expose the streaming boundaries.
• compileRaw_movedHeadFormula_eq_schedule proves literal raw-list equality.

@[simp]

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

One in-range direction block has its advertised numeric size.

@[simp]

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

The complete forward member phase is the prefix sum of its three sizes.

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

A natural direction counter and in-block offset recover the corresponding member gate.

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

Offsets before the effect-size boundary select the effect child stream.

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

The next fixed-width offsets select the predecessor-head child stream.

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

The final offset of each direction block is its conjunction gate.

@[simp]

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

The complete stream is members, one false identity, and three connectors.

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

The gate after the forward member phase is the false identity.

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

Connector rank is a natural upward counter visiting direction members in reverse order.

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

Exact raw compilation order of a non-halted moved-head formula.