Circuits for bounded Turing-machine traces

This module exposes the complete bounded-trace fragment: an initialized one-hot configuration followed by one packed transition layer per choice bit. Its final configuration occupies a contiguous block at the end of the fragment. The construction is topologically well formed at positive primary arity and has machine-dependent cubic size in the trace horizon.

Main results

• length_traceFragment: exact gate count.
• traceOutputEnd_eq: the final configuration block ends with the fragment.
• traceFragment_topologicallyWellFormed: every reference points backward.
• evalAux?_traceFragment: evaluation encodes the complete bounded trace.
• traceFragmentSize_le: a machine-dependent cubic gate-count bound.

@[simp]

theorem Complexity.CircuitUnrolling.length_traceFragment {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : List.length (traceFragment tm T n available layout) = traceFragmentSize tm T n available layout

A complete bounded-trace fragment emits exactly its recursively recorded gate count.

theorem Complexity.CircuitUnrolling.traceOutputEnd_eq {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : traceOutputBase tm T n available layout + configWidth tm T = available + traceFragmentSize tm T n available layout

The final packed configuration block ends exactly at the end of the trace fragment.

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

A complete trace fragment is topologically well formed whenever its primary-wire prefix is nonempty.

theorem Complexity.CircuitUnrolling.evalAux?_traceFragment {k : ℕ} (tm : NTM k) (T n available : ℕ) [NeZero available] (layout : InputWires T n available) (x : BitString n) (choices : Fin T → Bool) (wires : Array Bool) (hsize : wires.size = available) (hdata : ∀ (j : Fin n), wires[↑(layout.data j)]? = some (x j)) (hchoices : ∀ (j : Fin T), wires[↑(layout.choice j)]? = some (choices j)) : ∃ (result : Array Bool), (traceFragment tm T n available layout).evalAux? wires = some result ∧ result.size = wires.size + traceFragmentSize tm T n available layout ∧ (∀ j < wires.size, result[j]? = wires[j]?) ∧ EncodesConfig tm T (traceOutputBase tm T n available layout) result (tm.trace T choices (tm.initCfg x.toList))

Evaluating a complete trace fragment appends its exact gate count, preserves the primary-wire prefix, and packs the final bounded machine configuration.

theorem Complexity.CircuitUnrolling.traceFragmentSize_le {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : traceFragmentSize tm T n available layout ≤ traceSizeCoeff tm * (T + 2) ^ 3

The complete bounded trace has a machine-dependent cubic gate count in the trace horizon.