Numeric schedules for transition-effect formulas

This module exposes the case-indexed raw stream for effectFormula. The machine-dependent transition table is reduced to compile-time Boolean and natural-number oracles. Selected cases use the numeric case schedule, unselected cases emit one false gate, and a numeric reverse-OR suffix completes the disjunction.

Main results

• length_effectFormulaSchedule gives the exact numeric gate count.
• getElem_effectFormulaSchedule_identity and getElem_effectFormulaSchedule_connector identify the final fold phases.
• compileRaw_effectFormula_eq_schedule proves literal raw-list equality.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_effectFormulaCaseBlock (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (caseIndex : ℕ) (hcase : caseIndex < caseCount) : List.length (effectFormulaCaseBlock caseCount stateCount workCount T configBase choiceWire available selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt caseIndex) = effectFormulaSizeAt caseCount workCount T selectedAt choiceAt caseIndex

An in-range case block has exactly the size advertised by the total numeric case-size oracle.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_effectFormulaCaseGates (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (effectFormulaCaseGates caseCount stateCount workCount T configBase choiceWire available selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = prefixSize (effectFormulaSizeAt caseCount workCount T selectedAt choiceAt) caseCount

The forward member phase has the prefix-sum of all numeric case sizes.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_effectFormulaSchedule (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : List.length (effectFormulaSchedule caseCount stateCount workCount T configBase choiceWire available selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt) = effectFormulaScheduleSize caseCount workCount T selectedAt choiceAt

The complete effect schedule is all member gates, one false identity, and one connector per case.

theorem Complexity.CircuitUnrolling.Serializer.getElem_effectFormulaSchedule_identity (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : (effectFormulaSchedule caseCount stateCount workCount T configBase choiceWire available selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt)[prefixSize (effectFormulaSizeAt caseCount workCount T selectedAt choiceAt) caseCount] = CircuitCode.RawGate.constant 0 false

The gate immediately after all case blocks is the false disjunction identity.

theorem Complexity.CircuitUnrolling.Serializer.getElem_effectFormulaSchedule_connector (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (rank : Fin caseCount) : (effectFormulaSchedule caseCount stateCount workCount T configBase choiceWire available selectedAt choiceAt stateIndexAt inputSymbolIndexAt outputSymbolIndexAt workSymbolIndexAt)[prefixSize (effectFormulaSizeAt caseCount workCount T selectedAt choiceAt) caseCount + 1 + ↑rank] = indexedRightFoldConnector AndOrOp.or available caseCount (effectFormulaSizeAt caseCount workCount T selectedAt choiceAt) ↑rank

Connector rank is an upward natural counter visiting source cases in reverse order.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_effectFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (selects : TransitionEffect tm → Bool) : BoolFormula.compileRaw available (effectFormula tm T configBase choiceWire selects) = effectFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k T configBase choiceWire available (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm)

Exact raw compilation order of a transition-effect formula. All dynamic schedule inputs are natural numbers or Booleans; the machine-dependent case table is fixed by tm.