Structural internals for parallel amplification circuits

This file proves the exact fold invariants of the proof-free acceptance-copy builder. Raw-list length is the single source of gate accounting. The main results locate completed verdict wires and bound the complete amplified circuit by one cubic unrolling per run plus a quadratic majority threshold.

theorem Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild_zero_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : prefixAcceptanceCopiesBuild tm runs T n primaryAvailable 0 layout = initialAcceptanceCopiesBuild runs

The zero-copy prefix is the empty initial build.

theorem Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild_succ_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable i : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) (hi : i < runs) : prefixAcceptanceCopiesBuild tm runs T n primaryAvailable (i + 1) layout = acceptanceCopiesBuildStep tm layout (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout) ⟨i, hi⟩

Advancing a proper prefix appends exactly the acceptance copy indexed by the old prefix length.

theorem Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild_all_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : prefixAcceptanceCopiesBuild tm runs T n primaryAvailable runs layout = acceptanceCopiesBuild tm runs T n primaryAvailable layout

Taking the full run prefix recovers the complete copy build.

theorem Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild_succ_circuit_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable i : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) (hi : i < runs) : (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable (i + 1) layout).circuit = (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).circuit ++ acceptanceRawCircuit tm T n ((prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).available primaryAvailable) ((layout.run ⟨i, hi⟩).weaken (List.length (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).circuit))

Circuit projection of the canonical prefix recurrence.

theorem Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild_succ_available_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable i : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) (hi : i < runs) : (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable (i + 1) layout).available primaryAvailable = (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).available primaryAvailable + List.length (acceptanceRawCircuit tm T n ((prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).available primaryAvailable) ((layout.run ⟨i, hi⟩).weaken (List.length (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).circuit)))

First-unused-wire projection of the canonical prefix recurrence.

theorem Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild_succ_verdict_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable i : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) (hi : i < runs) : (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable (i + 1) layout).verdictWires ⟨i, hi⟩ = (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).available primaryAvailable + List.length (acceptanceRawCircuit tm T n ((prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).available primaryAvailable) ((layout.run ⟨i, hi⟩).weaken (List.length (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).circuit))) - 1

A newly completed run records the last wire of its acceptance fragment.

theorem Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild_succ_verdict_of_ne_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable i : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) (hi : i < runs) (j : Fin runs) (hji : j ≠ ⟨i, hi⟩) : (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable (i + 1) layout).verdictWires j = (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).verdictWires j

Completing run i leaves every other verdict entry unchanged.

theorem Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild_available_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable i : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).available primaryAvailable = primaryAvailable + List.length (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).circuit

A prefix's first unused wire is exactly its primary prefix plus its raw circuit length.

theorem Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild_verdict_bounds_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable i : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) (hi : i ≤ runs) (j : Fin runs) (hj : ↑j < i) : primaryAvailable ≤ (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).verdictWires j ∧ (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).verdictWires j < (prefixAcceptanceCopiesBuild tm runs T n primaryAvailable i layout).available primaryAvailable

Every completed verdict lies in the emitted-gate interval: at or after the primary prefix and strictly before the prefix build's first unused wire.

theorem Complexity.CircuitUnrolling.acceptanceCopiesVerdictWires_bounds_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) (j : Fin runs) : primaryAvailable ≤ acceptanceCopiesVerdictWires tm runs T n primaryAvailable layout j ∧ acceptanceCopiesVerdictWires tm runs T n primaryAvailable layout j < primaryAvailable + acceptanceCopiesSize tm runs T n primaryAvailable layout

Every complete verdict reference names a gate emitted by the copy build.

theorem Complexity.CircuitUnrolling.acceptanceCopiesBuildFrom_length_le_internal {k : ℕ} (tm : NTM k) {runs T n primaryAvailable : ℕ} (layout : ParallelInputWires runs T n primaryAvailable) (build : AcceptanceCopiesBuild runs) (indices : List (Fin runs)) : List.length (acceptanceCopiesBuildFrom tm layout build indices).circuit ≤ List.length build.circuit + indices.length * (acceptanceSizeCoeff tm * (T + 2) ^ 3)

Folding acceptance copies adds at most one cubic unrolling bound per run index in the supplied list.

theorem Complexity.CircuitUnrolling.acceptanceCopiesSize_le_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : acceptanceCopiesSize tm runs T n primaryAvailable layout ≤ runs * (acceptanceSizeCoeff tm * (T + 2) ^ 3)

All acceptance copies together use at most runs times the cubic single-run gate bound.

theorem Complexity.CircuitUnrolling.length_amplifiedAcceptanceRawCircuit_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : List.length (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout) = acceptanceCopiesSize tm runs T n primaryAvailable layout + (3 + 2 * runs * strictMajorityThreshold runs)

Appending strict majority adds its exact unary-threshold gate count.

theorem Complexity.CircuitUnrolling.thresholdTableSize_le_square_internal (runs : ℕ) : 2 * runs * strictMajorityThreshold runs ≤ 2 * runs * runs

The strict-majority threshold table is bounded by 2 * runs² gates beyond its three fixed gates.

theorem Complexity.CircuitUnrolling.length_amplifiedAcceptanceRawCircuit_le_internal {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : List.length (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout) ≤ runs * (acceptanceSizeCoeff tm * (T + 2) ^ 3) + 3 + 2 * runs * runs

Parallel amplification has one cubic unrolling per run plus a quadratic strict-majority threshold.