Numeric transition-formula schedules -- proof internals

The proofs first align the fixed-width numeric member streams with sequential formula compilation, then reuse the numeric right-fold suffix. Formula syntax, bounded positions, tape slots, and symbols appear only in the final adapter theorems.

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

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

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

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

theorem Complexity.CircuitUnrolling.Serializer.length_readFormulaSchedule_internal (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_member_internal (stateCount tapeCount T configBase available tapeIndex symbolIndex : ℕ) (position : Fin (T + 1)) (offset : Fin 3) : (readFormulaSchedule stateCount tapeCount T configBase available tapeIndex symbolIndex)[↑position * 3 + ↑offset] = (readFormulaMemberBlock stateCount tapeCount T configBase available tapeIndex symbolIndex ↑position)[↑offset]

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

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

theorem Complexity.CircuitUnrolling.Serializer.getElem_predecessorHeadMemberGates_internal (stateCount T configBase tapeIndex target directionCode : ℕ) (source : Fin (T + 1)) : (predecessorHeadMemberGates stateCount T configBase tapeIndex target directionCode)[↑source] = predecessorHeadMemberGate stateCount T configBase tapeIndex target directionCode ↑source

theorem Complexity.CircuitUnrolling.Serializer.length_predecessorHeadFormulaSchedule_internal (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_member_internal (stateCount T configBase available tapeIndex target directionCode : ℕ) (source : Fin (T + 1)) : (predecessorHeadFormulaSchedule stateCount T configBase available tapeIndex target directionCode)[↑source] = predecessorHeadMemberGate stateCount T configBase tapeIndex target directionCode ↑source

theorem Complexity.CircuitUnrolling.Serializer.getElem_predecessorHeadFormulaSchedule_identity_internal (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_internal (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_internal {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)

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