Semantic correctness of one-step transition formulas

This file proves that the formulas for a bounded Turing-machine transition evaluate to the halted-or-successor configuration selected by one choice bit. The proofs first decode reads and complete local transition cases, then verify the head-movement and tape-write formulas atom by atom.

theorem Complexity.CircuitUnrolling.configVar_eval_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (atom : ConfigAtom tm T) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hconfig : ∀ (oldAtom : ConfigAtom tm T), assignment (configWire tm T base oldAtom) = ConfigAtom.value c oldAtom) : BoolFormula.eval assignment (configVar tm T base atom) = ConfigAtom.value c atom

theorem Complexity.CircuitUnrolling.haltVar_eval_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) : BoolFormula.eval assignment (haltVar tm T base) = decide (c.state = tm.qhalt)

theorem Complexity.CircuitUnrolling.readFormula_eval_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (tape : TapeSlot k) (symbol : Γ) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) (hhead : (TapeSlot.get c tape).head < T + 1) : BoolFormula.eval assignment (readFormula tm T base tape symbol) = decide ((TapeSlot.get c tape).read = symbol)

theorem Complexity.CircuitUnrolling.caseFormula_eval_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (view : TransitionCase tm) (choice : Bool) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hchoice : assignment choiceWire = choice) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) (hheads : HeadsLt T c) : BoolFormula.eval assignment (caseFormula tm T base choiceWire view) = decide (currentCase tm choice c = view)

theorem Complexity.CircuitUnrolling.effectFormula_eval_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (selects : TransitionEffect tm → Bool) (choice : Bool) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hchoice : assignment choiceWire = choice) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) (hheads : HeadsLt T c) : BoolFormula.eval assignment (effectFormula tm T base choiceWire selects) = selects (currentCase tm choice c).effect

theorem Complexity.CircuitUnrolling.selectedStateFormula_eval_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (state : tm.Q) (choice : Bool) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hchoice : assignment choiceWire = choice) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) (hheads : HeadsLt T c) : BoolFormula.eval assignment (selectedStateFormula tm T base choiceWire state) = decide ((currentCase tm choice c).effect.nextState = state)

theorem Complexity.CircuitUnrolling.selectedMoveFormula_eval_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : TapeSlot k) (direction : Dir3) (choice : Bool) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hchoice : assignment choiceWire = choice) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) (hheads : HeadsLt T c) : BoolFormula.eval assignment (selectedMoveFormula tm T base choiceWire tape direction) = decide ((currentCase tm choice c).effect.move tape = direction)

theorem Complexity.CircuitUnrolling.selectedWriteFormula_eval_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : WritableSlot k) (symbol : Γ) (choice : Bool) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hchoice : assignment choiceWire = choice) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) (hheads : HeadsLt T c) : BoolFormula.eval assignment (selectedWriteFormula tm T base choiceWire tape symbol) = decide (((currentCase tm choice c).effect.write tape).toΓ = symbol)

theorem Complexity.CircuitUnrolling.predecessorHeadFormula_eval_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (tape : TapeSlot k) (target : Fin (T + 1)) (direction : Dir3) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) (hhead : (TapeSlot.get c tape).head < T + 1) : BoolFormula.eval assignment (predecessorHeadFormula tm T base tape target direction) = decide (movedHeadPosition (TapeSlot.get c tape).head direction = ↑target)

theorem Complexity.CircuitUnrolling.movedHeadFormula_eval_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : TapeSlot k) (target : Fin (T + 1)) (choice : Bool) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hchoice : assignment choiceWire = choice) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) (hheads : HeadsLt T c) : BoolFormula.eval assignment (movedHeadFormula tm T base choiceWire tape target) = decide (movedHeadPosition (TapeSlot.get c tape).head ((currentCase tm choice c).effect.move tape) = ↑target)

theorem Complexity.CircuitUnrolling.headAtCellFormula_eval_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (tape : TapeSlot k) (position : Fin (T + 2)) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) (hheads : HeadsLt T c) : BoolFormula.eval assignment (headAtCellFormula tm T base tape position) = decide ((TapeSlot.get c tape).head = ↑position)

theorem Complexity.CircuitUnrolling.writtenCellFormula_eval_internal {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : WritableSlot k) (position : Fin (T + 2)) (symbol : Γ) (choice : Bool) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hchoice : assignment choiceWire = choice) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) (hheads : HeadsLt T c) : BoolFormula.eval assignment (writtenCellFormula tm T base choiceWire tape position symbol) = if (TapeSlot.get c tape.toTapeSlot).head = ↑position then decide (((currentCase tm choice c).effect.write tape).toΓ = symbol) else decide ((TapeSlot.get c tape.toTapeSlot).cells ↑position = symbol)

theorem Complexity.CircuitUnrolling.haltedOrFormula_eval_internal {k : ℕ} (tm : NTM k) (T base : ℕ) (oldValue nextValue : BoolFormula) (assignment : ℕ → Bool) (c : Cfg k tm.Q) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T base atom) = ConfigAtom.value c atom) : BoolFormula.eval assignment (haltedOrFormula tm T base oldValue nextValue) = if c.state = tm.qhalt then BoolFormula.eval assignment oldValue else BoolFormula.eval assignment nextValue

theorem Complexity.CircuitUnrolling.nextFormula_eval_internal {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