Single-tape simulation — simulator state type

The state type SimQ k Q of NTM.singleTapeSim (for a source machine with state type Q and k work tapes) and its Fintype/DecidableEq instances. See docs/A4-SingleTapeSimulation.md §4–5 for the phase semantics.

The instances are noncomputable by design: singleTapeSim is a noncomputable def, and synthesizing computable DecidableEq for the function-typed phase data (Fin k → Γ, Fin k → Γw × Dir3) hits Lean's product/Pi synthesis-size limit. Finite is a Prop and composes with no such limit, so we route through it (Fintype.ofFinite / Classical.decEq).

@[reducible, inline]

abbrev Complexity.NTM.SingleTape.SweepPos (k : ℕ) : Type

A sweep position: which tape's triple (Fin k) and which of its 3 cells (head-bit / sym-hi / sym-lo, as Fin 3). The tape index is Fin (k+1) — a finite type (so the state stays Finite) whose 0 is constructible even when k = 0; the slack index k is unused in normal sweeps, and updates into Fin k-indexed data are guarded by if h : t.val < k.

Equations

• Complexity.NTM.SingleTape.SweepPos k = (Fin (k + 1) × Fin 3)

@[reducible, inline]

abbrev Complexity.NTM.SingleTape.GatherData (k : ℕ) (Q : Type) : Type

GATHER-phase data: the simulated state q, the head symbols accumulated so far (acc), the input/output symbols read at macro-step start (kept for the δ computation and the ▷-dodge), the current sweep position, a flag for whether the current tape's head marker was seen in this triple, and the pending high symbol cell read.

Equations

• Complexity.NTM.SingleTape.GatherData k Q = (Q × (Fin k → Complexity.Γ) × Complexity.Γ × Complexity.Γ × Complexity.NTM.SingleTape.SweepPos k × Bool × Complexity.Γ)

@[reducible, inline]

abbrev Complexity.NTM.SingleTape.RewindData (k : ℕ) (Q : Type) : Type

REWIND-phase data (between GATHER and SCATTER): the next state q', the δ results carried leftward back to cell 1 — per-tape write+move action, the deferred output write/dir, input dir, original input/output symbols — and the initial rightCarry marking heads that were at position 0 (acc = ▷, forced right off ▷), whose new marker must be deposited at block 1 by SCATTER.

Equations

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

@[reducible, inline]

abbrev Complexity.NTM.SingleTape.Scatter1Data (k : ℕ) (Q : Type) : Type

SCATTER sweep-1 data (rightward: write new symbols, place stay/right markers, materialize): the carried δ results, the sweep position, the per-tape rightCarry (markers to deposit at the next block), isLeftMover (recorded for sweep 2), and a writeFlag (currently overwriting a head's symbol).

Equations

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

@[reducible, inline]

abbrev Complexity.NTM.SingleTape.Scatter2Data (k : ℕ) (Q : Type) : Type

SCATTER sweep-2 data (leftward: deposit left-movers, rewind to cell 1): the deferred commit info, the sweep position, the isLeftMover set (from sweep

1. and the per-tape leftCarry (markers to deposit at the next-left block).

Equations

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

@[reducible, inline]

abbrev Complexity.NTM.SingleTape.CommitData (Q : Type) : Type

COMMIT-phase data: the next simulated state and the deferred input/output actions (output write+dir, input dir) with the symbols originally read.

Equations

• Complexity.NTM.SingleTape.CommitData Q = (Q × Complexity.Γw × Complexity.Dir3 × Complexity.Dir3 × Complexity.Γ × Complexity.Γ)

@[reducible, inline]

abbrev Complexity.NTM.SingleTape.SimQ (k : ℕ) (Q : Type) : Type

The simulator's state type. Phases (see docs/A4): run → gather → rewind → scatter1 → scatter2 → commit → run, plus halt.

Equations

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

@[match_pattern]

def Complexity.NTM.SingleTape.SimQ.run {k : ℕ} {Q : Type} (q : Q) : SimQ k Q

Between macro-steps, about to simulate an N-step from state q.

Equations

• Complexity.NTM.SingleTape.SimQ.run q = Sum.inl q

@[match_pattern]

def Complexity.NTM.SingleTape.SimQ.gather {k : ℕ} {Q : Type} (d : GatherData k Q) : SimQ k Q

Rightward read sweep, gathering head symbols.

Equations

• Complexity.NTM.SingleTape.SimQ.gather d = Sum.inr (Sum.inl d)

@[match_pattern]

def Complexity.NTM.SingleTape.SimQ.rewind {k : ℕ} {Q : Type} (d : RewindData k Q) : SimQ k Q

Leftward rewind back to cell 1, carrying the δ results.

Equations

• Complexity.NTM.SingleTape.SimQ.rewind d = Sum.inr (Sum.inr (Sum.inl d))

@[match_pattern]

def Complexity.NTM.SingleTape.SimQ.scatter1 {k : ℕ} {Q : Type} (d : Scatter1Data k Q) : SimQ k Q

Rightward write/marker sweep (stay/right moves + materialize).

Equations

• Complexity.NTM.SingleTape.SimQ.scatter1 d = Sum.inr (Sum.inr (Sum.inr (Sum.inl d)))

@[match_pattern]

def Complexity.NTM.SingleTape.SimQ.scatter2 {k : ℕ} {Q : Type} (d : Scatter2Data k Q) : SimQ k Q

Leftward marker sweep (left moves) + final rewind.

Equations

• Complexity.NTM.SingleTape.SimQ.scatter2 d = Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inl d))))

@[match_pattern]

def Complexity.NTM.SingleTape.SimQ.commit {k : ℕ} {Q : Type} (d : CommitData Q) : SimQ k Q

Applying the deferred input/output actions.

Equations

• Complexity.NTM.SingleTape.SimQ.commit d = Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inl d)))))

@[match_pattern]

def Complexity.NTM.SingleTape.SimQ.halt {k : ℕ} {Q : Type} : SimQ k Q

The halt state.

Equations

• Complexity.NTM.SingleTape.SimQ.halt = Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inr ())))))

instance Complexity.NTM.SingleTape.instFiniteSimQ (k : ℕ) (Q : Type) [Fintype Q] : Finite (SimQ k Q)

Finite composes freely (a Prop), so this synthesizes despite the function-typed phase data — the seven wide summands just need a raised instance-search size.

@[implicit_reducible]

noncomputable instance Complexity.NTM.SingleTape.instFintypeSimQ (k : ℕ) (Q : Type) [Fintype Q] : Fintype (SimQ k Q)

Noncomputable Fintype via Finite — sidesteps the product/Pi DecidableEq synthesis limit.

Equations

• Complexity.NTM.SingleTape.instFintypeSimQ k Q = Fintype.ofFinite (Complexity.NTM.SingleTape.SimQ k Q)

@[implicit_reducible]

noncomputable instance Complexity.NTM.SingleTape.instDecidableEqSimQ (k : ℕ) (Q : Type) : DecidableEq (SimQ k Q)

Noncomputable decidable equality — only used inside proofs (trace/step reduce c.state = qhalt in Prop), never executed.

Equations

• Complexity.NTM.SingleTape.instDecidableEqSimQ k Q = Classical.decEq (Complexity.NTM.SingleTape.SimQ k Q)