Numeric transition-formula schedules

This module exposes natural-index schedules for the two horizon-length folds inside tableau transition formulas. Read members occupy three gates and predecessor-head members occupy one; both finish with a false identity gate and reverse disjunction connectors. Formula syntax appears only in the final proof adapters.

Main results

• compileRaw_readFormula_eq_schedule identifies every read-formula stream.
• compileRaw_predecessorHeadFormula_eq_schedule identifies every predecessor head stream.
• The length and getElem theorems expose their exact numeric phases.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.fixedWidthSizeAt_of_lt {count width index : ℕ} (hindex : index < count) : fixedWidthSizeAt count width index = width

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.fixedWidthSizeAt_of_ge {count width index : ℕ} (hindex : count ≤ index) : fixedWidthSizeAt count width index = 0

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_readFormulaMemberBlock (stateCount tapeCount T configBase available tapeIndex symbolIndex position : ℕ) : List.length (readFormulaMemberBlock stateCount tapeCount T configBase available tapeIndex symbolIndex position) = 3

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_readFormulaMemberGates (stateCount tapeCount T configBase available tapeIndex symbolIndex : ℕ) : List.length (readFormulaMemberGates stateCount tapeCount T configBase available tapeIndex symbolIndex) = 3 * (T + 1)

theorem Complexity.CircuitUnrolling.Serializer.getElem_readFormulaMemberGates (stateCount tapeCount T configBase available tapeIndex symbolIndex : ℕ) (position : Fin (T + 1)) (offset : Fin 3) : (readFormulaMemberGates stateCount tapeCount T configBase available tapeIndex symbolIndex)[↑position * 3 + ↑offset] = (readFormulaMemberBlock stateCount tapeCount T configBase available tapeIndex symbolIndex ↑position)[↑offset]

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_readFormulaSchedule (stateCount tapeCount T configBase available tapeIndex symbolIndex : ℕ) : List.length (readFormulaSchedule stateCount tapeCount T configBase available tapeIndex symbolIndex) = 4 * (T + 1) + 1

theorem Complexity.CircuitUnrolling.Serializer.getElem_readFormulaSchedule_identity (stateCount tapeCount T configBase available tapeIndex symbolIndex : ℕ) : (readFormulaSchedule stateCount tapeCount T configBase available tapeIndex symbolIndex)[3 * (T + 1)] = CircuitCode.RawGate.constant 0 false

theorem Complexity.CircuitUnrolling.Serializer.getElem_readFormulaSchedule_connector (stateCount tapeCount T configBase available tapeIndex symbolIndex : ℕ) (rank : Fin (T + 1)) : (readFormulaSchedule stateCount tapeCount T configBase available tapeIndex symbolIndex)[3 * (T + 1) + 1 + ↑rank] = indexedRightFoldConnector AndOrOp.or available (T + 1) (fixedWidthSizeAt (T + 1) 3) ↑rank

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_predecessorHeadMemberGates (stateCount T configBase tapeIndex target directionCode : ℕ) : List.length (predecessorHeadMemberGates stateCount T configBase tapeIndex target directionCode) = T + 1

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_predecessorHeadFormulaSchedule (stateCount T configBase available tapeIndex target directionCode : ℕ) : List.length (predecessorHeadFormulaSchedule stateCount T configBase available tapeIndex target directionCode) = 2 * (T + 1) + 1

theorem Complexity.CircuitUnrolling.Serializer.getElem_predecessorHeadFormulaSchedule_identity (stateCount T configBase available tapeIndex target directionCode : ℕ) : (predecessorHeadFormulaSchedule stateCount T configBase available tapeIndex target directionCode)[T + 1] = CircuitCode.RawGate.constant 0 false

theorem Complexity.CircuitUnrolling.Serializer.getElem_predecessorHeadFormulaSchedule_connector (stateCount T configBase available tapeIndex target directionCode : ℕ) (rank : Fin (T + 1)) : (predecessorHeadFormulaSchedule stateCount T configBase available tapeIndex target directionCode)[T + 1 + 1 + ↑rank] = indexedRightFoldConnector AndOrOp.or available (T + 1) (fixedWidthSizeAt (T + 1) 1) ↑rank

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_readFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase available : ℕ) (tape : TapeSlot k) (symbol : Γ) : BoolFormula.compileRaw available (readFormula tm T configBase tape symbol) = readFormulaSchedule (Fintype.card tm.Q) (k + 2) T configBase available ↑tape.index ↑(symbolIndex symbol)

Exact raw compilation order of a horizon-length tape-read formula.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_predecessorHeadFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase available : ℕ) (tape : TapeSlot k) (target : Fin (T + 1)) (direction : Dir3) : BoolFormula.compileRaw available (predecessorHeadFormula tm T configBase tape target direction) = predecessorHeadFormulaSchedule (Fintype.card tm.Q) T configBase available (↑tape.index) (↑target) (match direction with | Dir3.left => 0 | Dir3.right => 1 | Dir3.stay => 2)

Exact raw compilation order of a horizon-length predecessor-head formula.