Packed circuit fragments for one Turing-machine transition

This module exposes an appendable raw circuit that evaluates every next-atom formula and packs the results into a contiguous successor-configuration block. The fragment preserves its input prefix, is topologically well formed, and has machine-dependent quadratic size in the trace horizon.

Main results

• length_stepFragment: exact fragment gate count.
• stepFragment_topologicallyWellFormed: all references point backward.
• evalAux?_stepFragment: exact packed successor-configuration semantics.
• stepFragmentSize_le: a machine-dependent quadratic size bound.

@[simp]

theorem Complexity.CircuitUnrolling.length_stepFormulas {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) : (stepFormulas tm T configBase choiceWire).length = configWidth tm T

The canonical next-formula list has one formula per configuration atom.

theorem Complexity.CircuitUnrolling.getElem_stepFormulas_configIndex {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) (atom : ConfigAtom tm T) : (stepFormulas tm T configBase choiceWire)[configIndex tm T atom] = nextFormula tm T configBase choiceWire atom

Looking up the canonical next-formula list by an atom's explicit index recovers that atom's transition formula.

@[simp]

theorem Complexity.CircuitUnrolling.length_stepFragment {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : List.length (stepFragment tm T configBase choiceWire available) = stepFragmentSize tm T configBase choiceWire

A packed one-step fragment emits exactly its named gate count.

@[simp]

theorem Complexity.CircuitUnrolling.configWire_stepOutputBase {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) (atom : ConfigAtom tm T) : configWire tm T (stepOutputBase tm T configBase choiceWire available) atom = stepOutputBase tm T configBase choiceWire available + configIndex tm T atom

Packed atom addresses are exactly configuration-wire addresses based at the packed successor block.

theorem Complexity.CircuitUnrolling.stepOutputEnd_eq {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : stepOutputBase tm T configBase choiceWire available + configWidth tm T = available + stepFragmentSize tm T configBase choiceWire

The packed successor block ends exactly at the end of the emitted fragment, so it can serve as the incoming block of the next unrolled step.

theorem Complexity.CircuitUnrolling.stepFragment_topologicallyWellFormed {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) [NeZero available] (hchoice : choiceWire < available) (hconfig : configBase + configWidth tm T ≤ available) : CircuitCode.RawCircuit.TopologicallyWellFormed available (stepFragment tm T configBase choiceWire available)

A packed step is topologically well formed when its choice wire and incoming configuration block lie in the existing prefix.

theorem Complexity.CircuitUnrolling.evalAux?_stepFragment {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) [NeZero available] (choice : Bool) (assignment : ℕ → Bool) (wires : Array Bool) (c : Cfg k tm.Q) (hsize : wires.size = available) (hinput : ∀ i < available, wires[i]? = some (assignment i)) (hchoice : assignment choiceWire = choice) (hconfig : ∀ (atom : ConfigAtom tm T), assignment (configWire tm T configBase atom) = ConfigAtom.value c atom) (hchoiceBound : choiceWire < available) (hconfigBound : configBase + configWidth tm T ≤ available) (hheads : HeadsLt T c) : ∃ (result : Array Bool), (stepFragment tm T configBase choiceWire available).evalAux? wires = some result ∧ result.size = wires.size + stepFragmentSize tm T configBase choiceWire ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ EncodesConfig tm T (stepOutputBase tm T configBase choiceWire available) result (choiceStep tm choice c)

Evaluating a packed step appends its exact gate count, preserves the input prefix, and packs an encoding of the selected successor configuration.

theorem Complexity.CircuitUnrolling.evalAux?_stepFragment_of_encodes {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) [NeZero available] (choice : Bool) (wires : Array Bool) (c : Cfg k tm.Q) (hsize : wires.size = available) (hchoice : wires[choiceWire]? = some choice) (hconfig : EncodesConfig tm T configBase wires c) (hchoiceBound : choiceWire < available) (hconfigBound : configBase + configWidth tm T ≤ available) (hheads : HeadsLt T c) : ∃ (result : Array Bool), (stepFragment tm T configBase choiceWire available).evalAux? wires = some result ∧ result.size = wires.size + stepFragmentSize tm T configBase choiceWire ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ EncodesConfig tm T (stepOutputBase tm T configBase choiceWire available) result (choiceStep tm choice c)

Evaluate a packed step directly from an encoded configuration and the concrete value stored at its choice wire.

theorem Complexity.CircuitUnrolling.stepFragmentSize_le {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) : stepFragmentSize tm T configBase choiceWire ≤ stepSizeCoeff tm * (T + 2) ^ 2

The exact packed one-step gate count is quadratic in the trace horizon, with a coefficient depending only on the fixed machine.

theorem Complexity.CircuitUnrolling.configWidth_le {k : ℕ} (tm : NTM k) (T : ℕ) : configWidth tm T ≤ (Fintype.card tm.Q + 5 * (k + 2)) * (T + 2)

A bounded configuration block has width linear in the trace horizon.