Circuit layouts for bounded Turing-machine traces

This file defines the wire layout used to unroll a bounded nondeterministic Turing-machine trace. A configuration is represented by one-hot atoms for its state, tape-head positions, and tape-cell symbols. Head positions range over Fin (T + 1) and cells over Fin (T + 2); the extra cell keeps output cell one present even at the zero-step horizon.

The primary-input layout is independent of the configuration layout. This lets later clients place random choices, data, and auxiliary inputs wherever they choose. prefixInputWires supplies the canonical choices-first order.

inductive Complexity.CircuitUnrolling.TapeSlot (k : ℕ) : Type

A named tape of a machine with k work tapes.

• input {k : ℕ} : TapeSlot k

  The read-only input tape.

• work {k : ℕ} (i : Fin k) : TapeSlot k

  One of the machine's work tapes.

• output {k : ℕ} : TapeSlot k

  The output tape.

def Complexity.CircuitUnrolling.instDecidableEqTapeSlot.decEq {k✝ : ℕ} (x✝ x✝¹ : TapeSlot k✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.instDecidableEqTapeSlot.decEq Complexity.CircuitUnrolling.TapeSlot.input Complexity.CircuitUnrolling.TapeSlot.input = isTrue ⋯
• Complexity.CircuitUnrolling.instDecidableEqTapeSlot.decEq Complexity.CircuitUnrolling.TapeSlot.input (Complexity.CircuitUnrolling.TapeSlot.work i) = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqTapeSlot.decEq Complexity.CircuitUnrolling.TapeSlot.input Complexity.CircuitUnrolling.TapeSlot.output = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqTapeSlot.decEq (Complexity.CircuitUnrolling.TapeSlot.work i) Complexity.CircuitUnrolling.TapeSlot.input = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqTapeSlot.decEq (Complexity.CircuitUnrolling.TapeSlot.work i) Complexity.CircuitUnrolling.TapeSlot.output = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqTapeSlot.decEq Complexity.CircuitUnrolling.TapeSlot.output Complexity.CircuitUnrolling.TapeSlot.input = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqTapeSlot.decEq Complexity.CircuitUnrolling.TapeSlot.output (Complexity.CircuitUnrolling.TapeSlot.work i) = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqTapeSlot.decEq Complexity.CircuitUnrolling.TapeSlot.output Complexity.CircuitUnrolling.TapeSlot.output = isTrue ⋯

@[implicit_reducible]

instance Complexity.CircuitUnrolling.instDecidableEqTapeSlot {k✝ : ℕ} : DecidableEq (TapeSlot k✝)

Equations

• Complexity.CircuitUnrolling.instDecidableEqTapeSlot = Complexity.CircuitUnrolling.instDecidableEqTapeSlot.decEq

@[implicit_reducible]

instance Complexity.CircuitUnrolling.instFintypeTapeSlot {k✝ : ℕ} : Fintype (TapeSlot k✝)

Equations

• Complexity.CircuitUnrolling.instFintypeTapeSlot = Fintype.ofEquiv (Unit ⊕ Fin k✝ ⊕ Unit) (Complexity.CircuitUnrolling.TapeSlot.proxyTypeEquiv k✝)

inductive Complexity.CircuitUnrolling.WritableSlot (k : ℕ) : Type

A named tape on which a machine transition may write.

• work {k : ℕ} (i : Fin k) : WritableSlot k

  One of the machine's work tapes.

• output {k : ℕ} : WritableSlot k

  The output tape.

@[implicit_reducible]

instance Complexity.CircuitUnrolling.instDecidableEqWritableSlot {k✝ : ℕ} : DecidableEq (WritableSlot k✝)

Equations

• Complexity.CircuitUnrolling.instDecidableEqWritableSlot = Complexity.CircuitUnrolling.instDecidableEqWritableSlot.decEq

def Complexity.CircuitUnrolling.instDecidableEqWritableSlot.decEq {k✝ : ℕ} (x✝ x✝¹ : WritableSlot k✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.instDecidableEqWritableSlot.decEq (Complexity.CircuitUnrolling.WritableSlot.work i) Complexity.CircuitUnrolling.WritableSlot.output = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqWritableSlot.decEq Complexity.CircuitUnrolling.WritableSlot.output (Complexity.CircuitUnrolling.WritableSlot.work i) = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqWritableSlot.decEq Complexity.CircuitUnrolling.WritableSlot.output Complexity.CircuitUnrolling.WritableSlot.output = isTrue ⋯

@[implicit_reducible]

instance Complexity.CircuitUnrolling.instFintypeWritableSlot {k✝ : ℕ} : Fintype (WritableSlot k✝)

Equations

• Complexity.CircuitUnrolling.instFintypeWritableSlot = Fintype.ofEquiv (Fin k✝ ⊕ Unit) (Complexity.CircuitUnrolling.WritableSlot.proxyTypeEquiv k✝)

def Complexity.CircuitUnrolling.WritableSlot.index {k : ℕ} : WritableSlot k → Fin (k + 1)

The zero-based position of a writable tape in work/output order.

Equations

• (Complexity.CircuitUnrolling.WritableSlot.work a).index = ⟨↑a, ⋯⟩
• Complexity.CircuitUnrolling.WritableSlot.output.index = ⟨k, ⋯⟩

def Complexity.CircuitUnrolling.WritableSlot.toTapeSlot {k : ℕ} : WritableSlot k → TapeSlot k

Regard a writable work/output slot as a general named tape slot.

Equations

• (Complexity.CircuitUnrolling.WritableSlot.work a).toTapeSlot = Complexity.CircuitUnrolling.TapeSlot.work a
• Complexity.CircuitUnrolling.WritableSlot.output.toTapeSlot = Complexity.CircuitUnrolling.TapeSlot.output

def Complexity.CircuitUnrolling.TapeSlot.index {k : ℕ} : TapeSlot k → Fin (k + 2)

The zero-based position of a named tape in input/work/output order.

Equations

• Complexity.CircuitUnrolling.TapeSlot.input.index = ⟨0, ⋯⟩
• (Complexity.CircuitUnrolling.TapeSlot.work a).index = ⟨↑a + 1, ⋯⟩
• Complexity.CircuitUnrolling.TapeSlot.output.index = ⟨k + 1, ⋯⟩

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

Select a named tape from a machine configuration.

Equations

• Complexity.CircuitUnrolling.TapeSlot.get c Complexity.CircuitUnrolling.TapeSlot.input = c.input
• Complexity.CircuitUnrolling.TapeSlot.get c (Complexity.CircuitUnrolling.TapeSlot.work a) = c.work a
• Complexity.CircuitUnrolling.TapeSlot.get c Complexity.CircuitUnrolling.TapeSlot.output = c.output

def Complexity.CircuitUnrolling.symbolIndex : Γ → Fin 4

The zero-based index of an alphabet symbol in zero/one/blank/start order.

Equations

• Complexity.CircuitUnrolling.symbolIndex Complexity.Γ.zero = ⟨0, Complexity.CircuitUnrolling.symbolIndex._proof_4⟩
• Complexity.CircuitUnrolling.symbolIndex Complexity.Γ.one = ⟨1, Complexity.CircuitUnrolling.symbolIndex._proof_6⟩
• Complexity.CircuitUnrolling.symbolIndex Complexity.Γ.blank = ⟨2, Complexity.CircuitUnrolling.symbolIndex._proof_8⟩
• Complexity.CircuitUnrolling.symbolIndex Complexity.Γ.start = ⟨3, Complexity.CircuitUnrolling.symbolIndex._proof_10⟩

inductive Complexity.CircuitUnrolling.ConfigAtom {k : ℕ} (tm : NTM k) (T : ℕ) : Type

A one-hot proposition about a bounded machine configuration.

• state {k : ℕ} {tm : NTM k} {T : ℕ} (q : tm.Q) : ConfigAtom tm T

  The machine is in the indicated state.

• head {k : ℕ} {tm : NTM k} {T : ℕ} (tape : TapeSlot k) (position : Fin (T + 1)) : ConfigAtom tm T

  A named tape's head is at the indicated position.

• cell {k : ℕ} {tm : NTM k} {T : ℕ} (tape : TapeSlot k) (position : Fin (T + 2)) (symbol : Γ) : ConfigAtom tm T

  A named tape's cell contains the indicated symbol.

@[implicit_reducible]

instance Complexity.CircuitUnrolling.instDecidableEqConfigAtom {k✝ : ℕ} {tm✝ : NTM k✝} {T✝ : ℕ} : DecidableEq (ConfigAtom tm✝ T✝)

Equations

• Complexity.CircuitUnrolling.instDecidableEqConfigAtom = Complexity.CircuitUnrolling.instDecidableEqConfigAtom.decEq

def Complexity.CircuitUnrolling.instDecidableEqConfigAtom.decEq {k✝ : ℕ} {tm✝ : NTM k✝} {T✝ : ℕ} (x✝ x✝¹ : ConfigAtom tm✝ T✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.instDecidableEqConfigAtom.decEq (Complexity.CircuitUnrolling.ConfigAtom.state q) (Complexity.CircuitUnrolling.ConfigAtom.head tape position) = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqConfigAtom.decEq (Complexity.CircuitUnrolling.ConfigAtom.state q) (Complexity.CircuitUnrolling.ConfigAtom.cell tape position symbol) = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqConfigAtom.decEq (Complexity.CircuitUnrolling.ConfigAtom.head tape position) (Complexity.CircuitUnrolling.ConfigAtom.state q) = isFalse ⋯
• Complexity.CircuitUnrolling.instDecidableEqConfigAtom.decEq (Complexity.CircuitUnrolling.ConfigAtom.cell tape position symbol) (Complexity.CircuitUnrolling.ConfigAtom.state q) = isFalse ⋯

def Complexity.CircuitUnrolling.configWidth {k : ℕ} (tm : NTM k) (T : ℕ) : ℕ

Number of Boolean wires in one bounded configuration block.

Equations

• Complexity.CircuitUnrolling.configWidth tm T = Fintype.card tm.Q + (k + 2) * (T + 1) + 4 * (k + 2) * (T + 2)

def Complexity.CircuitUnrolling.configAtomSumEquiv {k : ℕ} (tm : NTM k) (T : ℕ) : ConfigAtom tm T ≃ tm.Q ⊕ TapeSlot k × Fin (T + 1) ⊕ (TapeSlot k × Fin (T + 2)) × Γ

State/head/cell sum representation used to construct the explicit layout.

Equations

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

noncomputable def Complexity.CircuitUnrolling.tapeSlotEquiv (k : ℕ) : TapeSlot k ≃ Fin (k + 2)

Named tapes are explicitly equivalent to their input/work/output indices.

Equations

• Complexity.CircuitUnrolling.tapeSlotEquiv k = Equiv.ofBijective Complexity.CircuitUnrolling.TapeSlot.index ⋯

noncomputable def Complexity.CircuitUnrolling.symbolEquiv : Γ ≃ Fin 4

Alphabet symbols are explicitly equivalent to their four layout indices.

Equations

• Complexity.CircuitUnrolling.symbolEquiv = Equiv.ofBijective Complexity.CircuitUnrolling.symbolIndex Complexity.CircuitUnrolling.symbolEquiv._proof_3

noncomputable def Complexity.CircuitUnrolling.headAtomEquiv (k T : ℕ) : TapeSlot k × Fin (T + 1) ≃ Fin ((k + 2) * (T + 1))

Tape-head atoms are explicitly equivalent to their contiguous layout indices.

Equations

• Complexity.CircuitUnrolling.headAtomEquiv k T = ((Complexity.CircuitUnrolling.tapeSlotEquiv k).prodCongr (Equiv.refl (Fin (T + 1)))).trans finProdFinEquiv

noncomputable def Complexity.CircuitUnrolling.cellAtomEquiv (k T : ℕ) : (TapeSlot k × Fin (T + 2)) × Γ ≃ Fin (4 * (k + 2) * (T + 2))

Tape-cell atoms are explicitly equivalent to their contiguous layout indices.

Equations

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

noncomputable def Complexity.CircuitUnrolling.configAtomEquiv {k : ℕ} (tm : NTM k) (T : ℕ) : ConfigAtom tm T ≃ Fin (configWidth tm T)

Explicit equivalence between configuration atoms and their block indices.

Equations

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

@[implicit_reducible]

noncomputable instance Complexity.CircuitUnrolling.instFintypeConfigAtom {k : ℕ} (tm : NTM k) (T : ℕ) : Fintype (ConfigAtom tm T)

Finite enumeration of configuration atoms in explicit wire order.

Equations

• Complexity.CircuitUnrolling.instFintypeConfigAtom tm T = Fintype.ofEquiv (Fin (Complexity.CircuitUnrolling.configWidth tm T)) (Complexity.CircuitUnrolling.configAtomEquiv tm T).symm

noncomputable def Complexity.CircuitUnrolling.stateIndex {k : ℕ} (tm : NTM k) (q : tm.Q) : ℕ

Zero-based index of a machine state in the fixed finite-state ordering.

Equations

• Complexity.CircuitUnrolling.stateIndex tm q = ↑((Fintype.equivFin tm.Q) q)

noncomputable def Complexity.CircuitUnrolling.configIndex {k : ℕ} (tm : NTM k) (T : ℕ) : ConfigAtom tm T → ℕ

Zero-based index of an atom within one configuration block.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.configIndex tm T (Complexity.CircuitUnrolling.ConfigAtom.state q) = Complexity.CircuitUnrolling.stateIndex tm q
• Complexity.CircuitUnrolling.configIndex tm T (Complexity.CircuitUnrolling.ConfigAtom.head tape position) = Fintype.card tm.Q + ↑tape.index * (T + 1) + ↑position

theorem Complexity.CircuitUnrolling.configAtomEquiv_apply_val {k : ℕ} (tm : NTM k) (T : ℕ) (atom : ConfigAtom tm T) : ↑((configAtomEquiv tm T) atom) = configIndex tm T atom

The explicit arithmetic index agrees with the atom-layout equivalence.

theorem Complexity.CircuitUnrolling.configIndex_lt {k : ℕ} (tm : NTM k) (T : ℕ) (atom : ConfigAtom tm T) : configIndex tm T atom < configWidth tm T

Every explicit atom index lies inside its configuration block.

@[simp]

theorem Complexity.CircuitUnrolling.configIndex_state {k : ℕ} (tm : NTM k) (T : ℕ) (q : tm.Q) : configIndex tm T (ConfigAtom.state q) = stateIndex tm q

State atoms occupy the first portion of a configuration block.

@[simp]

theorem Complexity.CircuitUnrolling.configIndex_head {k : ℕ} (tm : NTM k) (T : ℕ) (tape : TapeSlot k) (position : Fin (T + 1)) : configIndex tm T (ConfigAtom.head tape position) = Fintype.card tm.Q + ↑tape.index * (T + 1) + ↑position

Head atoms follow states, ordered first by tape and then position.

@[simp]

theorem Complexity.CircuitUnrolling.configIndex_cell {k : ℕ} (tm : NTM k) (T : ℕ) (tape : TapeSlot k) (position : Fin (T + 2)) (symbol : Γ) : configIndex tm T (ConfigAtom.cell tape position symbol) = Fintype.card tm.Q + (k + 2) * (T + 1) + (↑tape.index * (T + 2) + ↑position) * 4 + ↑(symbolIndex symbol)

Cell atoms follow heads, ordered by tape, position, and symbol.

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

Absolute wire carrying a configuration atom after a given prefix.

Equations

• Complexity.CircuitUnrolling.configWire tm T base atom = base + Complexity.CircuitUnrolling.configIndex tm T atom

def Complexity.CircuitUnrolling.ConfigAtom.value {k : ℕ} {tm : NTM k} {T : ℕ} (c : Cfg k tm.Q) (atom : ConfigAtom tm T) : Bool

Boolean truth value of an atom in a concrete configuration.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.ConfigAtom.value c (Complexity.CircuitUnrolling.ConfigAtom.state q) = decide (c.state = q)
• Complexity.CircuitUnrolling.ConfigAtom.value c (Complexity.CircuitUnrolling.ConfigAtom.head tape position) = decide ((Complexity.CircuitUnrolling.TapeSlot.get c tape).head = ↑position)

def Complexity.CircuitUnrolling.EncodesConfig {k : ℕ} (tm : NTM k) (T base : ℕ) (wires : Array Bool) (c : Cfg k tm.Q) : Prop

An array encodes a configuration at base when every atom wire has its semantic one-hot value.

Equations

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

structure Complexity.CircuitUnrolling.InputWires (T n available : ℕ) : Type

Locations of choice and input-data bits among an existing wire prefix.

• choice : Fin T → Fin available

  Wire carrying each nondeterministic choice bit.

• data : Fin n → Fin available

  Wire carrying each input-data bit.

def Complexity.CircuitUnrolling.prefixInputWires (T n : ℕ) : InputWires T n (T + n)

Canonical input order: all choice bits, followed by all input-data bits.

Equations

• Complexity.CircuitUnrolling.prefixInputWires T n = { choice := fun (i : Fin T) => ⟨↑i, ⋯⟩, data := fun (i : Fin n) => ⟨T + ↑i, ⋯⟩ }

@[simp]

theorem Complexity.CircuitUnrolling.prefixInputWires_choice (T n : ℕ) (i : Fin T) : ↑((prefixInputWires T n).choice i) = ↑i

In the canonical layout, choice i is primary input wire i.

@[simp]

theorem Complexity.CircuitUnrolling.prefixInputWires_data (T n : ℕ) (i : Fin n) : ↑((prefixInputWires T n).data i) = T + ↑i

In the canonical layout, data bit i follows all T choice wires.

inductive Complexity.CircuitUnrolling.InitSource (available : ℕ) : Type

A Boolean source used by the one-gate initialization fragment.

• constant {available : ℕ} (value : Bool) : InitSource available

  A constant Boolean value.

• wire {available : ℕ} (input : Fin available) (negated : Bool) : InitSource available

  An existing wire, optionally negated.

def Complexity.CircuitUnrolling.InitSource.value {available : ℕ} (assignment : Fin available → Bool) : InitSource available → Bool

Semantic value of an initialization source under a prefix assignment.

Equations

• Complexity.CircuitUnrolling.InitSource.value assignment (Complexity.CircuitUnrolling.InitSource.constant value) = value
• Complexity.CircuitUnrolling.InitSource.value assignment (Complexity.CircuitUnrolling.InitSource.wire input negated) = (negated ^^ assignment input)

def Complexity.CircuitUnrolling.InitSource.gate {available : ℕ} : InitSource available → CircuitCode.RawGate

Compile an initialization source to exactly one raw gate.

Equations

• (Complexity.CircuitUnrolling.InitSource.constant value).gate = Complexity.CircuitCode.RawGate.constant 0 value
• (Complexity.CircuitUnrolling.InitSource.wire input negated).gate = Complexity.CircuitCode.RawGate.copy (↑input) negated

def Complexity.CircuitUnrolling.initSource {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : ConfigAtom tm T → InitSource available

Source for the initial one-hot value of a bounded configuration atom.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.initSource tm T n available layout (Complexity.CircuitUnrolling.ConfigAtom.state q) = Complexity.CircuitUnrolling.InitSource.constant (decide (tm.qstart = q))

noncomputable def Complexity.CircuitUnrolling.configAtoms {k : ℕ} (tm : NTM k) (T : ℕ) : List (ConfigAtom tm T)

Configuration atoms listed in exactly their explicit wire order.

Equations

• Complexity.CircuitUnrolling.configAtoms tm T = List.ofFn ⇑(Complexity.CircuitUnrolling.configAtomEquiv tm T).symm

noncomputable def Complexity.CircuitUnrolling.initFragment {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : CircuitCode.RawCircuit

One-gate-per-atom fragment producing the initial configuration block.

Equations

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