Boolean formulas for one Turing-machine transition

This file defines the proof-free formula layer for one step of a bounded nondeterministic Turing-machine trace. A TransitionCase records a complete local view of the machine, including its choice bit. Its TransitionEffect names the otherwise deeply nested components returned by NTM.δ.

The formulas read one encoded configuration block and produce the value of each atom in its halted-or-successor configuration. Input cells are preserved, writable cell zero is immutable, writes use the old head position, and head movement uses saturated subtraction at the left boundary. A right move from the largest represented head position has no represented target; clients rule out that case with HeadsLt before applying transition correctness.

def Complexity.CircuitUnrolling.WritableSlot.get {k : ℕ} {Q : Type} (c : Cfg k Q) : WritableSlot k → Tape

Select a writable work/output tape from a machine configuration.

Equations

• Complexity.CircuitUnrolling.WritableSlot.get c (Complexity.CircuitUnrolling.WritableSlot.work i) = c.work i
• Complexity.CircuitUnrolling.WritableSlot.get c Complexity.CircuitUnrolling.WritableSlot.output = c.output

structure Complexity.CircuitUnrolling.TransitionCase {k : ℕ} (tm : NTM k) : Type

A complete finite local view determining one nondeterministic transition.

• choice : Bool

  The nondeterministic or probabilistic choice bit for this step.

• state : tm.Q

  The current control state.

• inputRead : Γ

  The symbol under the input head.

• workRead : Fin k → Γ

  The symbol under each work-tape head.

• outputRead : Γ

  The symbol under the output head.

theorem Complexity.CircuitUnrolling.TransitionCase.ext {k : ℕ} {tm : NTM k} {x y : TransitionCase tm} (choice : x.choice = y.choice) (state : x.state = y.state) (inputRead : x.inputRead = y.inputRead) (workRead : x.workRead = y.workRead) (outputRead : x.outputRead = y.outputRead) : x = y

theorem Complexity.CircuitUnrolling.TransitionCase.ext_iff {k : ℕ} {tm : NTM k} {x y : TransitionCase tm} : x = y ↔ x.choice = y.choice ∧ x.state = y.state ∧ x.inputRead = y.inputRead ∧ x.workRead = y.workRead ∧ x.outputRead = y.outputRead

def Complexity.CircuitUnrolling.instDecidableEqTransitionCase.decEq {k✝ : ℕ} {tm✝ : NTM k✝} (x✝ x✝¹ : TransitionCase tm✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.CircuitUnrolling.instDecidableEqTransitionCase {k✝ : ℕ} {tm✝ : NTM k✝} : DecidableEq (TransitionCase tm✝)

Equations

• Complexity.CircuitUnrolling.instDecidableEqTransitionCase = Complexity.CircuitUnrolling.instDecidableEqTransitionCase.decEq

def Complexity.CircuitUnrolling.transitionCaseEquiv {k : ℕ} (tm : NTM k) : TransitionCase tm ≃ Bool × tm.Q × Γ × (Fin k → Γ) × Γ

Product representation used to enumerate complete local views.

Equations

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

@[implicit_reducible]

noncomputable instance Complexity.CircuitUnrolling.instFintypeTransitionCase {k : ℕ} (tm : NTM k) : Fintype (TransitionCase tm)

Complete local transition views form a finite type.

Equations

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

def Complexity.CircuitUnrolling.TransitionCase.read {k : ℕ} {tm : NTM k} (view : TransitionCase tm) : TapeSlot k → Γ

Select the read symbol for a named tape from a transition case.

Equations

• view.read Complexity.CircuitUnrolling.TapeSlot.input = view.inputRead
• view.read (Complexity.CircuitUnrolling.TapeSlot.work i) = view.workRead i
• view.read Complexity.CircuitUnrolling.TapeSlot.output = view.outputRead

def Complexity.CircuitUnrolling.currentCase {k : ℕ} (tm : NTM k) (choice : Bool) (c : Cfg k tm.Q) : TransitionCase tm

The complete local transition view presented by a configuration and choice bit.

Equations

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

structure Complexity.CircuitUnrolling.TransitionEffect {k : ℕ} (tm : NTM k) : Type

The named components of the action returned by NTM.δ for a local view.

• nextState : tm.Q

  The successor control state.

• workWrite : Fin k → Γw

  The symbol written on each work tape before its head moves.

• outputWrite : Γw

  The symbol written on the output tape before its head moves.

• inputMove : Dir3

  The input-head movement.

• workMove : Fin k → Dir3

  Each work-head movement.

• outputMove : Dir3

  The output-head movement.

@[implicit_reducible]

instance Complexity.CircuitUnrolling.instDecidableEqTransitionEffect {k✝ : ℕ} {tm✝ : NTM k✝} : DecidableEq (TransitionEffect tm✝)

Equations

• Complexity.CircuitUnrolling.instDecidableEqTransitionEffect = Complexity.CircuitUnrolling.instDecidableEqTransitionEffect.decEq

def Complexity.CircuitUnrolling.instDecidableEqTransitionEffect.decEq {k✝ : ℕ} {tm✝ : NTM k✝} (x✝ x✝¹ : TransitionEffect tm✝) : Decidable (x✝ = x✝¹)

Equations

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

def Complexity.CircuitUnrolling.TransitionEffect.write {k : ℕ} {tm : NTM k} (effect : TransitionEffect tm) : WritableSlot k → Γw

Select the write symbol for a named writable tape.

Equations

• effect.write (Complexity.CircuitUnrolling.WritableSlot.work i) = effect.workWrite i
• effect.write Complexity.CircuitUnrolling.WritableSlot.output = effect.outputWrite

def Complexity.CircuitUnrolling.TransitionEffect.move {k : ℕ} {tm : NTM k} (effect : TransitionEffect tm) : TapeSlot k → Dir3

Select the movement of any named tape head.

Equations

• effect.move Complexity.CircuitUnrolling.TapeSlot.input = effect.inputMove
• effect.move (Complexity.CircuitUnrolling.TapeSlot.work i) = effect.workMove i
• effect.move Complexity.CircuitUnrolling.TapeSlot.output = effect.outputMove

def Complexity.CircuitUnrolling.TransitionCase.effect {k : ℕ} {tm : NTM k} (view : TransitionCase tm) : TransitionEffect tm

Unpack the transition action selected by a complete local view.

Equations

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

noncomputable def Complexity.CircuitUnrolling.transitionCases {k : ℕ} (tm : NTM k) : List (TransitionCase tm)

Every possible local view, in the finite ordering induced by Fintype.

Equations

• Complexity.CircuitUnrolling.transitionCases tm = Finset.univ.toList

def Complexity.CircuitUnrolling.HeadsLt {k : ℕ} {Q : Type} (T : ℕ) (c : Cfg k Q) : Prop

Every named head lies strictly below T.

For the layout with head positions Fin (T + 1), this excludes the sole position whose right successor would fall outside the represented block.

Equations

• Complexity.CircuitUnrolling.HeadsLt T c = ∀ (tape : Complexity.CircuitUnrolling.TapeSlot k), (Complexity.CircuitUnrolling.TapeSlot.get c tape).head < T

def Complexity.CircuitUnrolling.choiceStep {k : ℕ} (tm : NTM k) (choice : Bool) (c : Cfg k tm.Q) : Cfg k tm.Q

Execute the halted-or-one-step semantics selected by one choice bit.

Equations

• Complexity.CircuitUnrolling.choiceStep tm choice c = tm.trace 1 (fun (x : Fin 1) => choice) c

noncomputable def Complexity.CircuitUnrolling.configVar {k : ℕ} (tm : NTM k) (T base : ℕ) (atom : ConfigAtom tm T) : BoolFormula

The formula variable carrying an atom of the incoming configuration.

Equations

• Complexity.CircuitUnrolling.configVar tm T base atom = Complexity.BoolFormula.var (Complexity.CircuitUnrolling.configWire tm T base atom)

noncomputable def Complexity.CircuitUnrolling.haltVar {k : ℕ} (tm : NTM k) (T base : ℕ) : BoolFormula

The incoming configuration's halted-state bit.

Equations

• Complexity.CircuitUnrolling.haltVar tm T base = Complexity.CircuitUnrolling.configVar tm T base (Complexity.CircuitUnrolling.ConfigAtom.state tm.qhalt)

def Complexity.CircuitUnrolling.headCellPosition {T : ℕ} (position : Fin (T + 1)) : Fin (T + 2)

Embed a represented head position into the one-cell-larger cell range.

Equations

• Complexity.CircuitUnrolling.headCellPosition position = ⟨↑position, ⋯⟩

noncomputable def Complexity.CircuitUnrolling.readFormula {k : ℕ} (tm : NTM k) (T base : ℕ) (tape : TapeSlot k) (symbol : Γ) : BoolFormula

Formula saying that a named tape reads a given symbol under its head.

Equations

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

noncomputable def Complexity.CircuitUnrolling.caseFormula {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (view : TransitionCase tm) : BoolFormula

Formula recognizing one complete local transition case.

Equations

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

noncomputable def Complexity.CircuitUnrolling.effectFormula {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (selects : TransitionEffect tm → Bool) : BoolFormula

Select transition cases whose named effect satisfies a Boolean test.

Equations

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

noncomputable def Complexity.CircuitUnrolling.selectedStateFormula {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (state : tm.Q) : BoolFormula

Formula selecting transition cases with a specified successor state.

Equations

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

noncomputable def Complexity.CircuitUnrolling.selectedMoveFormula {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : TapeSlot k) (direction : Dir3) : BoolFormula

Formula selecting transition cases that move a named head in a given direction.

Equations

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

noncomputable def Complexity.CircuitUnrolling.selectedWriteFormula {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : WritableSlot k) (symbol : Γ) : BoolFormula

Formula selecting transition cases that write a specified symbol.

Equations

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

def Complexity.CircuitUnrolling.movedHeadPosition (position : ℕ) : Dir3 → ℕ

Numeric head position after one move, with saturated movement at zero.

Equations

• Complexity.CircuitUnrolling.movedHeadPosition position Complexity.Dir3.left = position - 1
• Complexity.CircuitUnrolling.movedHeadPosition position Complexity.Dir3.right = position + 1
• Complexity.CircuitUnrolling.movedHeadPosition position Complexity.Dir3.stay = position

noncomputable def Complexity.CircuitUnrolling.predecessorHeadFormula {k : ℕ} (tm : NTM k) (T base : ℕ) (tape : TapeSlot k) (target : Fin (T + 1)) (direction : Dir3) : BoolFormula

Incoming head positions that reach a target under one fixed direction.

Equations

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

noncomputable def Complexity.CircuitUnrolling.movedHeadFormula {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : TapeSlot k) (target : Fin (T + 1)) : BoolFormula

Non-halted formula for a named head's next represented position.

Equations

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

noncomputable def Complexity.CircuitUnrolling.headAtCellFormula {k : ℕ} (tm : NTM k) (T base : ℕ) (tape : TapeSlot k) (position : Fin (T + 2)) : BoolFormula

Formula saying that the old head is at a represented cell position.

The final cell in Fin (T + 2) has no corresponding old head position and therefore produces false.

Equations

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

noncomputable def Complexity.CircuitUnrolling.haltedOrFormula {k : ℕ} (tm : NTM k) (T base : ℕ) (oldValue nextValue : BoolFormula) : BoolFormula

Choose the old atom when halted and a transition formula otherwise.

Equations

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

noncomputable def Complexity.CircuitUnrolling.writtenCellFormula {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) (tape : WritableSlot k) (position : Fin (T + 2)) (symbol : Γ) : BoolFormula

Formula for a positive writable cell after the write phase of one step.

Equations

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

noncomputable def Complexity.CircuitUnrolling.nextFormula {k : ℕ} (tm : NTM k) (T base choiceWire : ℕ) : ConfigAtom tm T → BoolFormula

Formula for one atom of the halted-or-successor configuration.

Input cells never change. Writable cell zero also never changes, because Tape.write is a no-op there. Every other writable cell is updated at the old head position before the head movement represented by the head atoms.

Equations

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