Boolean formulas for one Turing-machine transition

This module exposes the semantic and variable-support guarantees for the auditable transition formulas defined in Transition.Defs. A formula for one configuration atom reads only its designated choice bit and the preceding configuration block, and evaluates to that atom's value after one halted-or- successor machine step.

Main results

• nextFormula_eval: semantic correctness of every next-atom formula.
• mem_vars_nextFormula: exact source family of every referenced variable.
• vars_nextFormula_lt: all references lie in a sufficiently large prefix.

theorem Complexity.CircuitUnrolling.nextFormula_eval {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (atom : ConfigAtom tm T) (choice : Bool) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hchoice : assignment choiceWire = choice) (hconfig : ∀ (oldAtom : ConfigAtom tm T), assignment (configWire tm T base oldAtom) = ConfigAtom.value c oldAtom) (hheads : HeadsLt T c) : BoolFormula.eval assignment (nextFormula tm T base choiceWire atom) = ConfigAtom.value (choiceStep tm choice c) atom

A next-atom formula evaluates to the corresponding atom of the selected halted-or-successor configuration.

theorem Complexity.CircuitUnrolling.mem_vars_nextFormula {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (atom : ConfigAtom tm T) (i : ℕ) (hi : i ∈ (nextFormula tm T base choiceWire atom).vars) : i = choiceWire ∨ ∃ (oldAtom : ConfigAtom tm T), i = configWire tm T base oldAtom

Every next-atom formula variable is either its choice wire or a wire in the incoming configuration block.

theorem Complexity.CircuitUnrolling.vars_nextFormula_lt {k : ℕ} (tm : NTM k) (T base choiceWire available : ℕ) (atom : ConfigAtom tm T) (hchoice : choiceWire < available) (hconfig : base + configWidth tm T ≤ available) (i : ℕ) : i ∈ (nextFormula tm T base choiceWire atom).vars → i < available

If the choice wire and incoming configuration block lie in a prefix, every variable of a next-atom formula lies in that prefix.