Circuit unrolling for bounded Turing-machine traces

This module exposes the auditable wire layout, initialization layer, packed one-step transition compiler, and complete bounded-trace tiling for nondeterministic Turing machines. The tiled fragment has exact evaluation and topology laws together with a machine-dependent cubic size bound. A final gate selects the exact halt-and-output acceptance predicate, and the resulting raw code reconstructs to a typed single-output circuit. Parallel copies can share the data input, consume disjoint choice blocks, and feed a strict-majority threshold with an explicit polynomial gate bound.

@[simp]

theorem Complexity.CircuitUnrolling.length_configAtoms {k : ℕ} (tm : NTM k) (T : ℕ) : (configAtoms tm T).length = configWidth tm T

The canonical atom list has exactly one entry for every wire in a configuration block.

theorem Complexity.CircuitUnrolling.getElem_configAtoms_configIndex {k : ℕ} (tm : NTM k) (T : ℕ) (atom : ConfigAtom tm T) : (configAtoms tm T)[configIndex tm T atom] = atom

Looking up an atom at its explicit index in the canonical ordering recovers that atom.

@[simp]

theorem Complexity.CircuitUnrolling.length_initFragment {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : List.length (initFragment tm T n available layout) = configWidth tm T

Initialization emits exactly one raw gate per configuration atom.

theorem Complexity.CircuitUnrolling.initFragment_topologicallyWellFormed {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) : CircuitCode.RawCircuit.TopologicallyWellFormed available (initFragment tm T n available layout)

Every gate of the initialization fragment refers to an existing input wire, hence the fragment is topologically well formed at its prefix.

theorem Complexity.CircuitUnrolling.evalAux?_sourceGates (available : ℕ) [NeZero available] (sources : List (InitSource available)) (assignment : Fin available → Bool) (wires : Array Bool) (hsize : wires.size = available) (hinput : ∀ (i : Fin available), wires[↑i]? = some (assignment i)) : ∃ (result : Array Bool), CircuitCode.RawCircuit.evalAux? (List.map InitSource.gate sources) wires = some result ∧ result.size = wires.size + sources.length ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ ∀ (j : ℕ) (hj : j < sources.length), result[available + j]? = some (InitSource.value assignment sources[j])

Evaluating any list of one-gate initialization sources appends exactly their values, preserves the existing prefix, and records each emitted value at its consecutive output wire.

theorem Complexity.CircuitUnrolling.evalAux?_initFragment {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) {wires : Array Bool} (hsize : wires.size = available) (x : BitString n) (hx : ∀ (i : Fin n), wires[↑(layout.data i)]? = some (x i)) : ∃ (result : Array Bool), (initFragment tm T n available layout).evalAux? wires = some result ∧ result.size = wires.size + configWidth tm T ∧ (∀ i < wires.size, result[i]? = wires[i]?) ∧ EncodesConfig tm T available result (tm.initCfg x.toList)

Initialization appends one atom wire per configuration proposition, preserves the complete existing prefix, and encodes the machine's initial configuration. Choice wires may occur in the prefix but are not inspected.