Numeric schedules for one packed transition step

This definitions layer streams one nextFormula schedule for every configuration atom and then emits the packed successor copies in the same order. Atom descriptors are exposed as natural-number oracles indexed by the canonical atom counter. The fixed machine and ConfigAtom occur only in the compile-time extractor definitions used by the literal adapter.

The run-time schedule state consists solely of natural numbers and Booleans: numeric atom fields, numeric transition-case fields, prefix sizes, and Boolean selection oracles.

def Complexity.CircuitUnrolling.Serializer.stepAtomCount (stateCount workCount T : ℕ) : ℕ

Numeric number of atoms in one bounded configuration.

Equations

• Complexity.CircuitUnrolling.Serializer.stepAtomCount stateCount workCount T = stateCount + (workCount + 2) * (T + 1) + 4 * (workCount + 2) * (T + 2)

noncomputable def Complexity.CircuitUnrolling.Serializer.stepConfigAtomAt {k : ℕ} (tm : NTM k) (T index : ℕ) : ConfigAtom tm T

Fixed compile-time atom lookup with an irrelevant start-state fallback outside the canonical range. It never appears in run-time schedule state.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.stepAtomKindAt {k : ℕ} (tm : NTM k) (T index : ℕ) : ℕ

Compile-time numeric atom-kind oracle.

Equations

• Complexity.CircuitUnrolling.Serializer.stepAtomKindAt tm T index = Complexity.CircuitUnrolling.Serializer.nextAtomKind (Complexity.CircuitUnrolling.Serializer.stepConfigAtomAt tm T index)

noncomputable def Complexity.CircuitUnrolling.Serializer.stepAtomStateIndexAt {k : ℕ} (tm : NTM k) (T index : ℕ) : ℕ

Compile-time numeric state-index oracle.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.stepAtomTapeIndexAt {k : ℕ} (tm : NTM k) (T index : ℕ) : ℕ

Compile-time numeric tape-index oracle.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.stepAtomPositionAt {k : ℕ} (tm : NTM k) (T index : ℕ) : ℕ

Compile-time numeric position oracle.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.stepAtomSymbolIndexAt {k : ℕ} (tm : NTM k) (T index : ℕ) : ℕ

Compile-time numeric symbol-index oracle.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.stepAtomEffectSelectedAt {k : ℕ} (tm : NTM k) (T atomIndex phase caseIndex : ℕ) : Bool

Compile-time atom/phase/case selection oracle.

Equations

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

def Complexity.CircuitUnrolling.Serializer.stepFormulaSizeAt (caseCount stateCount workCount T : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (atomIndex : ℕ) : ℕ

Exact next-formula size at a numeric atom index, with zero outside the canonical atom range.

Equations

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

def Complexity.CircuitUnrolling.Serializer.stepFormulaAvailable (caseCount stateCount workCount T available : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (atomIndex : ℕ) : ℕ

First absolute wire available to one numeric next-atom schedule.

Equations

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

def Complexity.CircuitUnrolling.Serializer.stepFormulaBlock (caseCount stateCount workCount T configBase choiceWire available haltStateIndex : ℕ) (kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (atomIndex : ℕ) : CircuitCode.RawCircuit

Numeric next-formula block at one canonical atom index.

Equations

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

def Complexity.CircuitUnrolling.Serializer.stepFormulaGates (caseCount stateCount workCount T configBase choiceWire available haltStateIndex : ℕ) (kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : CircuitCode.RawCircuit

Forward stream of every next-formula block in canonical atom order.

Equations

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

def Complexity.CircuitUnrolling.Serializer.stepFormulaOutputRef (caseCount stateCount workCount T available : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (atomIndex : ℕ) : ℕ

Absolute output reference of one compiled next formula.

Equations

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

def Complexity.CircuitUnrolling.Serializer.stepPackedCopyGate (caseCount stateCount workCount T available : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (atomIndex : ℕ) : CircuitCode.RawGate

Packed-output copy gate for one forward atom index.

Equations

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

def Complexity.CircuitUnrolling.Serializer.stepPackedCopies (caseCount stateCount workCount T available : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) : CircuitCode.RawCircuit

Forward packed-copy suffix in canonical atom order.

Equations

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

def Complexity.CircuitUnrolling.Serializer.stepScheduleOutputBase (caseCount stateCount workCount T available : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) : ℕ

First absolute wire of the packed successor-configuration block.

Equations

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

def Complexity.CircuitUnrolling.Serializer.stepScheduleOutputRef (caseCount stateCount workCount T available : ℕ) (kindAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (atomIndex : ℕ) : ℕ

Absolute packed successor wire of one canonical atom index.

Equations

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

def Complexity.CircuitUnrolling.Serializer.stepSchedule (caseCount stateCount workCount T configBase choiceWire available haltStateIndex : ℕ) (kindAt atomStateIndexAt atomTapeIndexAt atomPositionAt atomSymbolIndexAt : ℕ → ℕ) (selectedAt : ℕ → ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : CircuitCode.RawCircuit

Complete numeric packed one-step schedule.

Equations

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

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

Exact gate count of the complete numeric packed one-step schedule.

Equations

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