Evaluation of tiled bounded-trace circuits

This internal module proves a concrete-array invariant for every canonical prefix of a tiled trace. The invariant starts with the initialization fragment, appends one array-native transition fragment at a time, and keeps the current packed block synchronized with the corresponding NTM trace prefix. The complete-trace theorem is the horizon specialization.

theorem Complexity.CircuitUnrolling.evalAux?_prefixTraceBuild_internal {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)) (i : ℕ) (hi : i ≤ T) : ∃ (result : Array Bool), (prefixTraceBuild tm T n available i layout).circuit.evalAux? wires = some result ∧ result.size = (prefixTraceBuild tm T n available i layout).available ∧ (∀ j < wires.size, result[j]? = wires[j]?) ∧ EncodesConfig tm T (prefixTraceBuild tm T n available i layout).configBase result (tm.trace i (fun (j : Fin i) => choices ⟨↑j, ⋯⟩) (tm.initCfg x.toList))

Evaluating the first i layers succeeds and encodes the corresponding initialized trace prefix.

theorem Complexity.CircuitUnrolling.evalAux?_traceFragment_internal {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 the complete tiled trace appends its exact gate count, preserves the primary prefix, and encodes the final bounded NTM trace.