Numeric schedules for transition-effect formulas

An effect formula is a finite disjunction over the fixed transition cases of the compiled machine. This layer describes its raw stream using a natural case counter, Boolean selection and choice oracles, and natural state and symbol indices. Selected members use the numeric case-formula schedule; unselected members are single false gates.

The machine-dependent case table is inspected only by compile-time numeric extractors. The streaming schedule itself carries no transition case, effect, formula tree, bounded index, or list traversal state.

noncomputable def Complexity.CircuitUnrolling.Serializer.effectCaseSelectedAt {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (caseIndex : ℕ) : Bool

Numeric selection bit of one fixed machine transition case.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.effectCaseChoiceAt {k : ℕ} (tm : NTM k) (caseIndex : ℕ) : Bool

Numeric choice bit of one fixed machine transition case.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.effectCaseStateIndexAt {k : ℕ} (tm : NTM k) (caseIndex : ℕ) : ℕ

Numeric state index of one fixed machine transition case.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.effectCaseInputSymbolIndexAt {k : ℕ} (tm : NTM k) (caseIndex : ℕ) : ℕ

Numeric input-symbol index of one fixed machine transition case.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.effectCaseOutputSymbolIndexAt {k : ℕ} (tm : NTM k) (caseIndex : ℕ) : ℕ

Numeric output-symbol index of one fixed machine transition case.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.effectCaseWorkSymbolIndexAt {k : ℕ} (tm : NTM k) (caseIndex workIndex : ℕ) : ℕ

Numeric work-symbol index of one fixed case and work-tape position.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitUnrolling.Serializer.effectFormulaCaseSize (workCount T : ℕ) (selected choiceValue : Bool) : ℕ

Gate count of one effect-disjunction member.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitUnrolling.Serializer.effectFormulaSizeAt (caseCount workCount T : ℕ) (selectedAt choiceAt : ℕ → Bool) (caseIndex : ℕ) : ℕ

Total numeric case-size oracle, returning zero beyond caseCount.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitUnrolling.Serializer.effectFormulaCaseAvailable (caseCount workCount T available : ℕ) (selectedAt choiceAt : ℕ → Bool) (caseIndex : ℕ) : ℕ

First gate position of one case member in the effect disjunction.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitUnrolling.Serializer.effectFormulaCaseBlock (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (caseIndex : ℕ) : CircuitCode.RawCircuit

Numeric raw fragment for one effect-disjunction member.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitUnrolling.Serializer.effectFormulaCaseGates (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : CircuitCode.RawCircuit

Forward numeric stream of all effect-disjunction case members.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitUnrolling.Serializer.effectFormulaSchedule (caseCount stateCount workCount T configBase choiceWire available : ℕ) (selectedAt choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : CircuitCode.RawCircuit

Complete numeric raw schedule for a transition-effect formula.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitUnrolling.Serializer.effectFormulaScheduleSize (caseCount workCount T : ℕ) (selectedAt choiceAt : ℕ → Bool) : ℕ

Exact gate count of the complete numeric effect-formula schedule.

Equations

• One or more equations did not get rendered due to their size.