Documentation

Complexitylib.Classes.PPoly.Uniform.Unrolling.Serializer.Transition.Atomic

Numeric schedules for atomic transition formulas #

This module exposes the one-gate numeric head-at-cell schedule and the fixed postorder halted-or wrapper used by state, head, and writable-cell successors.

source
theorem Complexity.CircuitUnrolling.Serializer.compileRaw_headAtCellFormula_eq_gate {k : ℕ} (tm : NTM k) (T configBase available : ℕ) (tape : TapeSlot k) (position : Fin (T + 2)) :
BoolFormula.compileRaw available (headAtCellFormula tm T configBase tape position) = [headAtCellFormulaGate (Fintype.card tm.Q) T configBase ↑tape.index ↑position]

The natural head/cell indices literally reproduce the compiled head-at-cell formula.

source
theorem Complexity.CircuitUnrolling.Serializer.compileRaw_haltedOrFormula_eq_schedule {k : ℕ} (tm : NTM k) (T configBase available : ℕ) (oldValue nextValue : BoolFormula) :
BoolFormula.compileRaw available (haltedOrFormula tm T configBase oldValue nextValue) = haltedOrSchedule (configWire tm T configBase (ConfigAtom.state tm.qhalt)) available (BoolFormula.compileRaw (available + 1) oldValue) (BoolFormula.compileRaw (available + oldValue.size + 4) nextValue)

Formula compilation of the halted-or choice is exactly the fixed numeric wrapper around its two child schedules.