Topology of tiled bounded-trace circuits

This internal module proves that initialization followed by any sequence of packed transition layers is topologically well formed. The recursive proof tracks the exact circuit length, first unused wire, and end of the current configuration block supplied by the trace-structure layer.

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

The initial-configuration portion of a trace build is topologically well formed after its primary-wire prefix.

theorem Complexity.CircuitUnrolling.traceBuildStep_topologicallyWellFormed_internal {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} [NeZero primaryAvailable] (layout : InputWires T n primaryAvailable) (build : TraceBuild) (i : Fin T) (hwell : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable build.circuit) (hlength : List.length build.circuit = build.size) (havailable : build.available = primaryAvailable + build.size) (houtputEnd : build.configBase + configWidth tm T = build.available) : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable (traceBuildStep tm layout build i).circuit

Appending one packed transition preserves topology when the accumulated build records its exact length, end wire, and current configuration block.

theorem Complexity.CircuitUnrolling.traceBuildFrom_topologicallyWellFormed_internal {k : ℕ} (tm : NTM k) {T n primaryAvailable : ℕ} [NeZero primaryAvailable] (layout : InputWires T n primaryAvailable) (build : TraceBuild) (indices : List (Fin T)) (hwell : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable build.circuit) (hlength : List.length build.circuit = build.size) (havailable : build.available = primaryAvailable + build.size) (houtputEnd : build.configBase + configWidth tm T = build.available) : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable (traceBuildFrom tm layout build indices).circuit

Folding any list of transition indices preserves topology together with the trace build's structural invariants.

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

Every canonical partial trace build is topologically well formed.

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

The complete trace build is topologically well formed.

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

The complete bounded-trace fragment is topologically well formed after its primary-wire prefix.