Numeric schedules for next-configuration atoms

This layer gives the five branches of nextFormula a common numeric interface. An atom is represented by a natural kind code together with natural state, tape, position, and symbol indices. A phase-indexed Boolean oracle carries the fixed transition-case selection data needed by state, head, and positive writable-cell branches.

The run-time schedule contains only natural numbers and Booleans. The fixed machine and ConfigAtom appear solely in compile-time extractors used by the literal proof adapter.

def Complexity.CircuitUnrolling.Serializer.nextStateAtomKind : ℕ

Numeric kind code for state atoms.

Equations

• Complexity.CircuitUnrolling.Serializer.nextStateAtomKind = 0

def Complexity.CircuitUnrolling.Serializer.nextHeadAtomKind : ℕ

Numeric kind code for head atoms.

Equations

• Complexity.CircuitUnrolling.Serializer.nextHeadAtomKind = 1

def Complexity.CircuitUnrolling.Serializer.nextInputCellAtomKind : ℕ

Numeric kind code for immutable input-cell atoms.

Equations

• Complexity.CircuitUnrolling.Serializer.nextInputCellAtomKind = 2

def Complexity.CircuitUnrolling.Serializer.nextWritableMarkerAtomKind : ℕ

Numeric kind code for immutable writable marker-cell atoms.

Equations

• Complexity.CircuitUnrolling.Serializer.nextWritableMarkerAtomKind = 3

def Complexity.CircuitUnrolling.Serializer.nextWritableCellAtomKind : ℕ

Numeric kind code for positive writable-cell atoms.

Equations

• Complexity.CircuitUnrolling.Serializer.nextWritableCellAtomKind = 4

def Complexity.CircuitUnrolling.Serializer.nextAtomKind {k : ℕ} {tm : NTM k} {T : ℕ} : ConfigAtom tm T → ℕ

Numeric atom-kind extractor used only by the proof adapter.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.Serializer.nextAtomKind (Complexity.CircuitUnrolling.ConfigAtom.state q) = Complexity.CircuitUnrolling.Serializer.nextStateAtomKind
• Complexity.CircuitUnrolling.Serializer.nextAtomKind (Complexity.CircuitUnrolling.ConfigAtom.head tape position) = Complexity.CircuitUnrolling.Serializer.nextHeadAtomKind

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

Numeric state index of a state atom; zero for every other atom kind.

Equations

• Complexity.CircuitUnrolling.Serializer.nextAtomStateIndex tm (Complexity.CircuitUnrolling.ConfigAtom.state state) = Complexity.CircuitUnrolling.stateIndex tm state
• Complexity.CircuitUnrolling.Serializer.nextAtomStateIndex tm x✝ = 0

def Complexity.CircuitUnrolling.Serializer.nextAtomTapeIndex {k : ℕ} {tm : NTM k} {T : ℕ} : ConfigAtom tm T → ℕ

Numeric tape index of a head or cell atom; zero for state atoms.

Equations

• Complexity.CircuitUnrolling.Serializer.nextAtomTapeIndex (Complexity.CircuitUnrolling.ConfigAtom.state q) = 0
• Complexity.CircuitUnrolling.Serializer.nextAtomTapeIndex (Complexity.CircuitUnrolling.ConfigAtom.head tape position) = ↑tape.index
• Complexity.CircuitUnrolling.Serializer.nextAtomTapeIndex (Complexity.CircuitUnrolling.ConfigAtom.cell tape position symbol) = ↑tape.index

def Complexity.CircuitUnrolling.Serializer.nextAtomPosition {k : ℕ} {tm : NTM k} {T : ℕ} : ConfigAtom tm T → ℕ

Numeric position of a head or cell atom; zero for state atoms.

Equations

• Complexity.CircuitUnrolling.Serializer.nextAtomPosition (Complexity.CircuitUnrolling.ConfigAtom.state q) = 0
• Complexity.CircuitUnrolling.Serializer.nextAtomPosition (Complexity.CircuitUnrolling.ConfigAtom.head tape position) = ↑position
• Complexity.CircuitUnrolling.Serializer.nextAtomPosition (Complexity.CircuitUnrolling.ConfigAtom.cell tape position symbol) = ↑position

def Complexity.CircuitUnrolling.Serializer.nextAtomSymbolIndex {k : ℕ} {tm : NTM k} {T : ℕ} : ConfigAtom tm T → ℕ

Numeric symbol index of a cell atom; zero for state and head atoms.

Equations

• Complexity.CircuitUnrolling.Serializer.nextAtomSymbolIndex (Complexity.CircuitUnrolling.ConfigAtom.cell tape position symbol) = ↑(Complexity.CircuitUnrolling.symbolIndex symbol)
• Complexity.CircuitUnrolling.Serializer.nextAtomSymbolIndex x✝ = 0

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

Numeric index of the fixed halted state.

Equations

• Complexity.CircuitUnrolling.Serializer.nextHaltStateIndex tm = Complexity.CircuitUnrolling.stateIndex tm tm.qhalt

noncomputable def Complexity.CircuitUnrolling.Serializer.nextAtomEffectSelectedAt {k : ℕ} (tm : NTM k) {T : ℕ} : ConfigAtom tm T → ℕ → ℕ → Bool

Compile-time transition selection data specialized to one atom.

Phase zero is used by state and writable-cell schedules; head schedules use the three movement-direction phase codes directly.

Equations

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

def Complexity.CircuitUnrolling.Serializer.nextFormulaChildAvailable (available : ℕ) : ℕ

The child of a halted-or wrapper begins five gates after the wrapper.

Equations

• Complexity.CircuitUnrolling.Serializer.nextFormulaChildAvailable available = available + 5

def Complexity.CircuitUnrolling.Serializer.nextAtomWire (stateCount tapeCount T configBase atomKind stateIndex tapeIndex position symbolIndex : ℕ) : ℕ

Numeric wire of the old atom selected by its kind and layout indices.

Equations

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

def Complexity.CircuitUnrolling.Serializer.nextHaltedOrSchedule (haltWire available oldWire : ℕ) (nextSchedule : CircuitCode.RawCircuit) : CircuitCode.RawCircuit

Halted-or wrapper specialized to a one-gate old-atom copy.

Equations

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

def Complexity.CircuitUnrolling.Serializer.nextHaltedOrScheduleSize (nextSize : ℕ) : ℕ

Exact size of a halted-or wrapper around a one-gate old atom.

Equations

• Complexity.CircuitUnrolling.Serializer.nextHaltedOrScheduleSize nextSize = nextSize + 7

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

Numeric schedule for a state atom.

Equations

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

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

Exact gate count of a numeric state-atom schedule.

Equations

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

def Complexity.CircuitUnrolling.Serializer.nextHeadFormulaSchedule (caseCount stateCount workCount T configBase choiceWire available tapeIndex target haltStateIndex : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : CircuitCode.RawCircuit

Numeric schedule for a head atom.

Equations

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

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

Exact gate count of a numeric head-atom schedule.

Equations

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

def Complexity.CircuitUnrolling.Serializer.nextCellCopySchedule (stateCount tapeCount T configBase tapeIndex position symbolIndex : ℕ) : CircuitCode.RawCircuit

One-gate schedule for an immutable input or writable marker cell.

Equations

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

def Complexity.CircuitUnrolling.Serializer.nextCellCopyScheduleSize : ℕ

Exact gate count of an immutable cell schedule.

Equations

• Complexity.CircuitUnrolling.Serializer.nextCellCopyScheduleSize = 1

def Complexity.CircuitUnrolling.Serializer.nextWrittenCellFormulaSchedule (caseCount stateCount workCount T configBase choiceWire available tapeIndex position symbolIndex haltStateIndex : ℕ) (selectedAt choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : CircuitCode.RawCircuit

Numeric schedule for a positive writable-cell atom.

Equations

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

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

Exact gate count of a positive writable-cell schedule.

Equations

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

def Complexity.CircuitUnrolling.Serializer.nextFormulaSchedule (caseCount stateCount workCount T configBase choiceWire available atomKind stateIndex tapeIndex position symbolIndex haltStateIndex : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (caseStateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : CircuitCode.RawCircuit

Common numeric schedule interface for all five next-atom branches.

selectedAt is phase-indexed: phase zero supplies state/write selection, while head atoms use direction phases zero through two.

Equations

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

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

Exact gate count selected by the common numeric atom-kind interface.

Equations

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