Parallel amplification circuits

This module exposes a circuit that runs several independent bounded traces of one nondeterministic machine on shared input data and returns their strict majority verdict. The implementation serializes the copies in raw gate order, but every copy reads only its own choice block and the common data block.

The circuit layer deliberately stops at Fin.countP. Its interpretation as the randomized layer's blockMajority is supplied by Complexitylib.Classes.Randomized.CircuitAmplification.

Main results

• amplifiedAcceptanceRawCircuit_wellFormed: the raw circuit is valid.
• eval?_amplifiedAcceptanceRawCircuit: raw evaluation returns the threshold of the independent bounded acceptance bits.
• amplifiedAcceptanceCircuit_eval: typed reconstruction has the same semantics.
• canonicalAmplifiedAcceptanceCircuit_eval: choices-first canonical semantics.
• amplifiedAcceptanceCircuit_size_le: one cubic unrolling per run plus a quadratic threshold circuit.

@[simp]

theorem Complexity.CircuitUnrolling.length_amplifiedAcceptanceRawCircuit {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)

Exact gate count: all acceptance copies followed by the threshold fragment.

theorem Complexity.CircuitUnrolling.amplifiedAcceptanceRawCircuit_topologicallyWellFormed {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)

Every reference in the amplified raw circuit points backward.

theorem Complexity.CircuitUnrolling.amplifiedAcceptanceRawCircuit_wellFormed {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 amplified raw circuit is nonempty and topologically ordered.

theorem Complexity.CircuitUnrolling.length_amplifiedAcceptanceRawCircuit_le {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 uses one cubic trace circuit per run and one quadratic threshold circuit.

theorem Complexity.CircuitUnrolling.evalAux?_amplifiedAcceptanceRawCircuit {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) (x : BitString n) (choices : Fin runs → BitString T) (wires : Array Bool) (hsize : wires.size = primaryAvailable) (hdata : ∀ (j : Fin n), wires[↑(layout.data j)]? = some (x j)) (hchoices : ∀ (j : Fin runs) (t : Fin T), wires[↑(layout.choice j t)]? = some (choices j t)) : ∃ (result : Array Bool), (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout).evalAux? wires = some result ∧ result.size = wires.size + List.length (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout) ∧ (∀ j < wires.size, result[j]? = wires[j]?) ∧ result[amplifiedAcceptanceOutputWire tm runs T n primaryAvailable layout]? = some (decide (strictMajorityThreshold runs ≤ Fin.countP (parallelAcceptanceBits tm T x choices)))

Array-native evaluation appends the exact raw gate count, preserves the primary inputs, and records the threshold value at the designated output.

theorem Complexity.CircuitUnrolling.eval?_amplifiedAcceptanceRawCircuit {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) (x : BitString n) (choices : Fin runs → BitString T) (input : BitString primaryAvailable) (hdata : ∀ (j : Fin n), input (layout.data j) = x j) (hchoices : ∀ (j : Fin runs) (t : Fin T), input (layout.choice j t) = choices j t) : (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout).eval? input.toList = some (decide (strictMajorityThreshold runs ≤ Fin.countP (parallelAcceptanceBits tm T x choices)))

Raw single-output evaluation returns the strict-threshold predicate over the independent bounded acceptance bits.

noncomputable def Complexity.CircuitUnrolling.amplifiedAcceptanceCircuit {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) : Circuit Basis.andOr2 primaryAvailable 1 (List.length (amplifiedAcceptanceRawCircuit tm runs T n primaryAvailable layout) - 1)

Reconstruct a valid amplified raw circuit as a typed single-output circuit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.CircuitUnrolling.amplifiedAcceptanceCircuit_size {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) : (amplifiedAcceptanceCircuit tm runs T n primaryAvailable layout).size = acceptanceCopiesSize tm runs T n primaryAvailable layout + (3 + 2 * runs * strictMajorityThreshold runs)

Typed reconstruction preserves the exact amplified raw gate count.

theorem Complexity.CircuitUnrolling.amplifiedAcceptanceCircuit_size_le {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) : (amplifiedAcceptanceCircuit tm runs T n primaryAvailable layout).size ≤ runs * (acceptanceSizeCoeff tm * (T + 2) ^ 3) + 3 + 2 * runs * runs

The typed amplified circuit satisfies the same explicit polynomial bound.

theorem Complexity.CircuitUnrolling.amplifiedAcceptanceCircuit_eval {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) [NeZero primaryAvailable] (layout : ParallelInputWires runs T n primaryAvailable) (x : BitString n) (choices : Fin runs → BitString T) (input : BitString primaryAvailable) (hdata : ∀ (j : Fin n), input (layout.data j) = x j) (hchoices : ∀ (j : Fin runs) (t : Fin T), input (layout.choice j t) = choices j t) : (amplifiedAcceptanceCircuit tm runs T n primaryAvailable layout).eval input 0 = decide (strictMajorityThreshold runs ≤ Fin.countP (parallelAcceptanceBits tm T x choices))

Typed evaluation computes the threshold of the independent bounded runs.

noncomputable def Complexity.CircuitUnrolling.canonicalAmplifiedAcceptanceCircuit {k : ℕ} (tm : NTM k) (runs T n : ℕ) [NeZero (runs * T + n)] : Circuit Basis.andOr2 (runs * T + n) 1 (List.length (canonicalAmplifiedAcceptanceRawCircuit tm runs T n) - 1)

Canonical choices-first, shared-data-second amplified circuit.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.CircuitUnrolling.canonicalAmplifiedAcceptanceCircuit_eval {k : ℕ} (tm : NTM k) (runs T n : ℕ) [NeZero (runs * T + n)] (seed : BitString (runs * T)) (x : BitString n) : (canonicalAmplifiedAcceptanceCircuit tm runs T n).eval (Fin.append seed x) 0 = decide (strictMajorityThreshold runs ≤ Fin.countP (canonicalAcceptanceBits tm runs T x seed))

Under the canonical layout, typed evaluation consumes the flat seed before the shared input and returns the threshold of the named acceptance-bit vector.

theorem Complexity.CircuitUnrolling.canonicalAmplifiedAcceptanceCircuit_size_le {k : ℕ} (tm : NTM k) (runs T n : ℕ) [NeZero (runs * T + n)] : (canonicalAmplifiedAcceptanceCircuit tm runs T n).size ≤ runs * (acceptanceSizeCoeff tm * (T + 2) ^ 3) + 3 + 2 * runs * runs

The canonical typed circuit inherits the generic amplified size bound.