Numeric schedules for atomic transition formulas -- definitions

This layer removes two more formula-syntax seams from the direct serializer. headAtCellFormulaGate reconstructs its single raw gate from natural layout indices, while haltedOrSchedule gives the fixed postorder wrapper around already scheduled old-value and next-value fragments.

def Complexity.CircuitUnrolling.Serializer.headAtCellFormulaGate (stateCount T configBase tapeIndex position : ℕ) : CircuitCode.RawGate

Single numeric gate saying whether an old head occupies a cell position. The final cell, which has no represented old head, is constant false.

Equations

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

def Complexity.CircuitUnrolling.Serializer.haltedOrSchedule (haltWire available : ℕ) (oldSchedule nextSchedule : CircuitCode.RawCircuit) : CircuitCode.RawCircuit

Raw postorder wrapper for haltedOrFormula around two already compiled fragments. The old fragment begins after the first halt-wire copy; the next fragment begins after the complete left conjunct and the negated halt test.

Equations

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