Topology internals for parallel amplification circuits

Independent acceptance copies are appended after one shared primary-input prefix. Their recorded verdict wires then feed the final strict-majority threshold fragment. This file proves that both stages are topologically ordered and that the final nonempty raw circuit is well formed.

theorem Complexity.CircuitUnrolling.initialAcceptanceCopiesBuild_topologicallyWellFormed_internal (runs primaryAvailable : ℕ) : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable (initialAcceptanceCopiesBuild runs).circuit

The empty acceptance-copy build is topologically well formed.

theorem Complexity.CircuitUnrolling.acceptanceCopiesBuildStep_topologicallyWellFormed_internal {k : ℕ} (tm : NTM k) {runs T n primaryAvailable : ℕ} [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) (build : AcceptanceCopiesBuild runs) (j : Fin runs) (hbuild : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable build.circuit) : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable (acceptanceCopiesBuildStep tm layout build j).circuit

Appending one independent acceptance copy preserves topology.

theorem Complexity.CircuitUnrolling.acceptanceCopiesBuildFrom_topologicallyWellFormed_internal {k : ℕ} (tm : NTM k) {runs T n primaryAvailable : ℕ} [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) (build : AcceptanceCopiesBuild runs) (indices : List (Fin runs)) (hbuild : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable build.circuit) : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable (acceptanceCopiesBuildFrom tm layout build indices).circuit

Folding any sequence of run indices preserves copy topology.

theorem Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild_topologicallyWellFormed_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable i : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).circuit

Every canonical prefix of the acceptance-copy fold is topologically ordered after the shared primary-input prefix.

theorem Complexity.CircuitUnrolling.acceptanceCopiesBuild_topologicallyWellFormed_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable (acceptanceCopiesBuild tm runs T n primaryAvailable layout).circuit

The complete collection of independent acceptance copies is topologically ordered.

theorem Complexity.CircuitUnrolling.amplifiedAcceptanceRawCircuit_topologicallyWellFormed_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) : CircuitCode.RawCircuit.TopologicallyWellFormed primaryAvailable (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout)

The acceptance copies followed by their strict-majority threshold are topologically ordered after any nonempty primary prefix.

theorem Complexity.CircuitUnrolling.amplifiedAcceptanceRawCircuit_wellFormed_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) : CircuitCode.RawCircuit.WellFormed primaryAvailable (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout)

The final threshold fragment is nonempty, so amplified topology upgrades to full raw-circuit well-formedness.