Structural properties of tiled bounded-trace circuits

This internal module proves that the recursive trace layout tracks its exact gate count and first unused wire. It also identifies the final packed configuration block and derives a machine-dependent cubic size bound.

theorem Complexity.CircuitUnrolling.initialTraceBuild_length_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : List.length (initialTraceBuild tm T n available layout).circuit = (initialTraceBuild tm T n available layout).size

Initialization records its exact emitted gate count.

theorem Complexity.CircuitUnrolling.initialTraceBuild_available_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : (initialTraceBuild tm T n available layout).available = available + (initialTraceBuild tm T n available layout).size

Initialization's first unused wire is its primary prefix plus its size.

theorem Complexity.CircuitUnrolling.initialTraceBuild_outputEnd_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : (initialTraceBuild tm T n available layout).configBase + configWidth tm T = (initialTraceBuild tm T n available layout).available

The initialized configuration block ends at the first unused wire.

theorem Complexity.CircuitUnrolling.traceBuildStep_length_internal {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} (layout : InputWires T n primaryAvailable) (build : TraceBuild) (i : Fin T) (hbuild : List.length build.circuit = build.size) : List.length (traceBuildStep tm layout build i).circuit = (traceBuildStep tm layout build i).size

Appending one layer preserves the exact circuit-length invariant.

theorem Complexity.CircuitUnrolling.traceBuildStep_available_internal {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} (layout : InputWires T n primaryAvailable) (build : TraceBuild) (i : Fin T) (hbuild : build.available = primaryAvailable + build.size) : (traceBuildStep tm layout build i).available = primaryAvailable + (traceBuildStep tm layout build i).size

Appending one layer preserves the primary-prefix/end-wire invariant.

theorem Complexity.CircuitUnrolling.traceBuildStep_outputEnd_internal {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} (layout : InputWires T n primaryAvailable) (build : TraceBuild) (i : Fin T) : (traceBuildStep tm layout build i).configBase + configWidth tm T = (traceBuildStep tm layout build i).available

A newly packed successor block ends at the new first unused wire.

theorem Complexity.CircuitUnrolling.traceBuildFrom_length_internal {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} (layout : InputWires T n primaryAvailable) (build : TraceBuild) (indices : List (Fin T)) (hbuild : List.length build.circuit = build.size) : List.length (traceBuildFrom tm layout build indices).circuit = (traceBuildFrom tm layout build indices).size

Folding transition indices preserves the exact circuit-length invariant.

theorem Complexity.CircuitUnrolling.traceBuildFrom_available_internal {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} (layout : InputWires T n primaryAvailable) (build : TraceBuild) (indices : List (Fin T)) (hbuild : build.available = primaryAvailable + build.size) : (traceBuildFrom tm layout build indices).available = primaryAvailable + (traceBuildFrom tm layout build indices).size

Folding transition indices preserves the primary-prefix/end-wire invariant.

theorem Complexity.CircuitUnrolling.traceBuildFrom_outputEnd_internal {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} (layout : InputWires T n primaryAvailable) (build : TraceBuild) (indices : List (Fin T)) (hbuild : build.configBase + configWidth tm T = build.available) : (traceBuildFrom tm layout build indices).configBase + configWidth tm T = (traceBuildFrom tm layout build indices).available

A folded sequence leaves its final packed block at the circuit end.

theorem Complexity.CircuitUnrolling.traceBuildFrom_size_le_internal {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} (layout : InputWires T n primaryAvailable) (build : TraceBuild) (indices : List (Fin T)) : (traceBuildFrom tm layout build indices).size ≤ build.size + indices.length * (stepSizeCoeff tm * (T + 2) ^ 2)

A folded sequence adds at most one quadratic layer bound per index.

theorem Complexity.CircuitUnrolling.prefixTraceBuild_zero_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : prefixTraceBuild tm T n available 0 layout = initialTraceBuild tm T n available layout

The zero-step prefix build is exactly the initialized configuration.

theorem Complexity.CircuitUnrolling.prefixTraceBuild_succ_internal {k : ℕ} (tm : NTM k) (T n available i : ℕ) (layout : InputWires T n available) (hi : i < T) : prefixTraceBuild tm T n available (i + 1) layout = traceBuildStep tm layout (prefixTraceBuild tm T n available i layout) ⟨i, hi⟩

Advancing a proper prefix appends exactly its indexed transition layer.

theorem Complexity.CircuitUnrolling.prefixTraceBuild_succ_circuit_internal {k : ℕ} (tm : NTM k) (T n available i : ℕ) (layout : InputWires T n available) (hi : i < T) : (prefixTraceBuild tm T n available (i + 1) layout).circuit = (prefixTraceBuild tm T n available i layout).circuit ++ stepFragment tm T (prefixTraceBuild tm T n available i layout).configBase (↑(layout.choice ⟨i, hi⟩)) (prefixTraceBuild tm T n available i layout).available

Circuit projection of the canonical prefix recurrence.

theorem Complexity.CircuitUnrolling.prefixTraceBuild_succ_configBase_internal {k : ℕ} (tm : NTM k) (T n available i : ℕ) (layout : InputWires T n available) (hi : i < T) : (prefixTraceBuild tm T n available (i + 1) layout).configBase = stepOutputBase tm T (prefixTraceBuild tm T n available i layout).configBase (↑(layout.choice ⟨i, hi⟩)) (prefixTraceBuild tm T n available i layout).available

Final-configuration-base projection of the canonical prefix recurrence.

theorem Complexity.CircuitUnrolling.prefixTraceBuild_succ_available_internal {k : ℕ} (tm : NTM k) (T n available i : ℕ) (layout : InputWires T n available) (hi : i < T) : (prefixTraceBuild tm T n available (i + 1) layout).available = (prefixTraceBuild tm T n available i layout).available + stepFragmentSize tm T (prefixTraceBuild tm T n available i layout).configBase ↑(layout.choice ⟨i, hi⟩)

End-wire projection of the canonical prefix recurrence.

theorem Complexity.CircuitUnrolling.prefixTraceBuild_succ_size_internal {k : ℕ} (tm : NTM k) (T n available i : ℕ) (layout : InputWires T n available) (hi : i < T) : (prefixTraceBuild tm T n available (i + 1) layout).size = (prefixTraceBuild tm T n available i layout).size + stepFragmentSize tm T (prefixTraceBuild tm T n available i layout).configBase ↑(layout.choice ⟨i, hi⟩)

Gate-count projection of the canonical prefix recurrence.

theorem Complexity.CircuitUnrolling.prefixTraceBuild_length_internal {k : ℕ} (tm : NTM k) (T n available i : ℕ) (layout : InputWires T n available) : List.length (prefixTraceBuild tm T n available i layout).circuit = (prefixTraceBuild tm T n available i layout).size

Every prefix build records its exact circuit length.

theorem Complexity.CircuitUnrolling.prefixTraceBuild_available_internal {k : ℕ} (tm : NTM k) (T n available i : ℕ) (layout : InputWires T n available) : (prefixTraceBuild tm T n available i layout).available = available + (prefixTraceBuild tm T n available i layout).size

Every prefix ends its recorded size after the primary input prefix.

theorem Complexity.CircuitUnrolling.prefixTraceBuild_outputEnd_internal {k : ℕ} (tm : NTM k) (T n available i : ℕ) (layout : InputWires T n available) : (prefixTraceBuild tm T n available i layout).configBase + configWidth tm T = (prefixTraceBuild tm T n available i layout).available

Every prefix's packed configuration block reaches its current end wire.

theorem Complexity.CircuitUnrolling.prefixTraceBuild_eq_traceBuild_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : prefixTraceBuild tm T n available T layout = traceBuild tm T n available layout

Taking all T canonical indices recovers the complete trace build.

theorem Complexity.CircuitUnrolling.traceBuild_length_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : List.length (traceBuild tm T n available layout).circuit = (traceBuild tm T n available layout).size

The complete trace build records its exact circuit length.

theorem Complexity.CircuitUnrolling.traceBuild_available_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : (traceBuild tm T n available layout).available = available + (traceBuild tm T n available layout).size

The complete trace ends exactly its recorded size after the primary prefix.

theorem Complexity.CircuitUnrolling.traceBuild_outputEnd_internal {k : ℕ} (tm : NTM k) (T n available : ℕ) (layout : InputWires T n available) : (traceBuild tm T n available layout).configBase + configWidth tm T = (traceBuild tm T n available layout).available

The complete trace's final packed configuration reaches the circuit end.

theorem Complexity.CircuitUnrolling.length_traceFragment_internal {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

Internal exact gate count of the complete bounded-trace fragment.

theorem Complexity.CircuitUnrolling.traceOutputEnd_eq_internal {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

Internal final-output block identity for the complete trace fragment.

theorem Complexity.CircuitUnrolling.traceFragmentSize_le_internal {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 machine-dependent cubic gate count.