Internal correctness of bounded-trace initialization circuits

This file proves the exact size, topological ordering, and iterative-evaluator semantics of the one-gate-per-atom initialization fragment.

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

Internal exact length of the canonical atom ordering.

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

Internal lookup law connecting arithmetic atom indices to list order.

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

Internal exact gate count of the initialization fragment.

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

Internal topological well-formedness of initialization gates.

theorem Complexity.CircuitUnrolling.evalAux?_sourceGates_internal (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])

Internal evaluator theorem for a list of one-gate initialization sources.

theorem Complexity.CircuitUnrolling.evalAux?_initFragment_internal {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)

Internal semantic correctness theorem for the initial-configuration fragment.