Numeric schedules for transition-case formulas

One fixed transition case is flattened into six numeric phases: a choice literal, one state-wire copy, one input read, a fixed finite list of work-tape reads, one output read, and the conjunction suffix. Machine/view data is compiled into natural indices and Boolean values before entering this layer. No formula tree, configuration atom, tape slot, symbol, or bounded position is stored by the schedule.

def Complexity.CircuitUnrolling.Serializer.caseChoiceLiteralSize : Bool → ℕ

Gate count of a compiled choice literal.

Equations

• Complexity.CircuitUnrolling.Serializer.caseChoiceLiteralSize true = 1
• Complexity.CircuitUnrolling.Serializer.caseChoiceLiteralSize false = 2

def Complexity.CircuitUnrolling.Serializer.caseChoiceLiteralSchedule (available choiceWire : ℕ) : Bool → CircuitCode.RawCircuit

Exact raw fragment for a compiled choice literal.

Equations

• Complexity.CircuitUnrolling.Serializer.caseChoiceLiteralSchedule available choiceWire true = [Complexity.CircuitCode.RawGate.copy choiceWire]
• Complexity.CircuitUnrolling.Serializer.caseChoiceLiteralSchedule available choiceWire false = [Complexity.CircuitCode.RawGate.copy choiceWire, Complexity.CircuitCode.RawGate.copy available true]

def Complexity.CircuitUnrolling.Serializer.caseReadSize (T : ℕ) : ℕ

Common gate count of every compiled tape-read formula.

Equations

• Complexity.CircuitUnrolling.Serializer.caseReadSize T = 4 * (T + 1) + 1

def Complexity.CircuitUnrolling.Serializer.caseFormulaMemberCount (workCount : ℕ) : ℕ

Number of conjuncts in a case with workCount work tapes.

Equations

• Complexity.CircuitUnrolling.Serializer.caseFormulaMemberCount workCount = workCount + 4

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

Number of gates in all case members, before the conjunction suffix.

Equations

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

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

Total number of gates in a compiled case formula.

Equations

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

def Complexity.CircuitUnrolling.Serializer.caseFormulaSizeAt (workCount T : ℕ) (choiceValue : Bool) (index : ℕ) : ℕ

Numeric member-size oracle in literal/state/input/work/output order.

Equations

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

def Complexity.CircuitUnrolling.Serializer.transitionStateRef (configBase stateIndex : ℕ) : ℕ

Absolute state-wire reference reconstructed from its numeric state index.

Equations

• Complexity.CircuitUnrolling.Serializer.transitionStateRef configBase stateIndex = configBase + stateIndex

def Complexity.CircuitUnrolling.Serializer.caseInputReadAvailable (available : ℕ) (choiceValue : Bool) : ℕ

First gate position of the input-read member.

Equations

• Complexity.CircuitUnrolling.Serializer.caseInputReadAvailable available choiceValue = available + Complexity.CircuitUnrolling.Serializer.caseChoiceLiteralSize choiceValue + 1

def Complexity.CircuitUnrolling.Serializer.caseWorkReadAvailable (T available workIndex : ℕ) (choiceValue : Bool) : ℕ

First gate position of one work-read member.

Equations

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

def Complexity.CircuitUnrolling.Serializer.caseOutputReadAvailable (workCount T available : ℕ) (choiceValue : Bool) : ℕ

First gate position of the output-read member.

Equations

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

def Complexity.CircuitUnrolling.Serializer.caseWorkReadGates (stateCount workCount T configBase available : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) : CircuitCode.RawCircuit

Fixed-width stream of all work-tape read members.

Equations

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

def Complexity.CircuitUnrolling.Serializer.caseFormulaMemberGates (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) : CircuitCode.RawCircuit

Forward member stream for one fixed transition case.

Equations

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

def Complexity.CircuitUnrolling.Serializer.caseFormulaSchedule (stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolAt : ℕ → ℕ) : CircuitCode.RawCircuit

Complete raw schedule for one fixed transition-case formula.

Equations

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