Parallel amplification circuits -- definitions

This definitions layer emits several independent copies of a bounded-trace acceptance circuit. Every copy reads the same data wires and its own block of choice wires. The copies are serialized consecutively in the raw code, but their semantics are parallel: each copy receives only the shared primary inputs assigned to it and records one verdict wire.

After all copies have been emitted, a unary threshold fragment computes their strict majority. The construction is proof-free. Later modules establish the exact gate count, topological ordering, and evaluation semantics.

def Complexity.CircuitUnrolling.InputWires.weaken {T n available : ℕ} (layout : InputWires T n available) (extra : ℕ) : InputWires T n (available + extra)

Regard an input layout as living in a larger prefix obtained by appending extra wires. The absolute locations of every existing input are unchanged.

Equations

• layout.weaken extra = { choice := fun (i : Fin T) => Fin.castLE ⋯ (layout.choice i), data := fun (i : Fin n) => Fin.castLE ⋯ (layout.data i) }

@[simp]

theorem Complexity.CircuitUnrolling.InputWires.weaken_choice_val {T n available : ℕ} (layout : InputWires T n available) (extra : ℕ) (i : Fin T) : ↑((layout.weaken extra).choice i) = ↑(layout.choice i)

Weakening an input layout does not change a choice wire's absolute index.

@[simp]

theorem Complexity.CircuitUnrolling.InputWires.weaken_data_val {T n available : ℕ} (layout : InputWires T n available) (extra : ℕ) (i : Fin n) : ↑((layout.weaken extra).data i) = ↑(layout.data i)

Weakening an input layout does not change a data wire's absolute index.

structure Complexity.CircuitUnrolling.ParallelInputWires (runs T n available : ℕ) : Type

Locations of several choice blocks and one shared data block in an existing wire prefix. Run j reads the choice map choice j and every run reads the same data map.

• choice : Fin runs → Fin T → Fin available

  Choice wire at a run index and a within-run time index.

• data : Fin n → Fin available

  Shared input-data wires.

def Complexity.CircuitUnrolling.ParallelInputWires.run {runs T n available : ℕ} (layout : ParallelInputWires runs T n available) (j : Fin runs) : InputWires T n available

Select one run's ordinary bounded-trace input layout.

Equations

• layout.run j = { choice := layout.choice j, data := layout.data }

@[simp]

theorem Complexity.CircuitUnrolling.ParallelInputWires.run_choice {runs T n available : ℕ} (layout : ParallelInputWires runs T n available) (j : Fin runs) (t : Fin T) : (layout.run j).choice t = layout.choice j t

Selecting a run recovers that run's choice map.

@[simp]

theorem Complexity.CircuitUnrolling.ParallelInputWires.run_data {runs T n available : ℕ} (layout : ParallelInputWires runs T n available) (j : Fin runs) (i : Fin n) : (layout.run j).data i = layout.data i

Selecting a run retains the shared data map.

def Complexity.CircuitUnrolling.prefixParallelInputWires (runs T n : ℕ) : ParallelInputWires runs T n (runs * T + n)

Canonical primary-input order for parallel amplification: all runs * T choice bits in row-major run/time order, followed by the shared n data bits.

Equations

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

@[simp]

theorem Complexity.CircuitUnrolling.prefixParallelInputWires_choice_val (runs T n : ℕ) (j : Fin runs) (t : Fin T) : ↑((prefixParallelInputWires runs T n).choice j t) = ↑t + T * ↑j

Canonical parallel choice wire (j, t) has row-major absolute index t + T * j.

@[simp]

theorem Complexity.CircuitUnrolling.prefixParallelInputWires_data_val (runs T n : ℕ) (i : Fin n) : ↑((prefixParallelInputWires runs T n).data i) = runs * T + ↑i

Canonical shared data starts immediately after every choice block.

structure Complexity.CircuitUnrolling.AcceptanceCopiesBuild (runs : ℕ) : Type

Accumulated raw code while emitting independent acceptance copies.

verdictWires has the final arity from the beginning, avoiding dependent casts while folding over run indices. Before run j is emitted its entry is a dummy value; prefix invariants only interpret entries for completed runs.

• circuit : CircuitCode.RawCircuit

  Acceptance fragments emitted so far.

• verdictWires : Fin runs → ℕ

  Absolute output wire assigned to each completed run.

def Complexity.CircuitUnrolling.AcceptanceCopiesBuild.available {runs : ℕ} (build : AcceptanceCopiesBuild runs) (primaryAvailable : ℕ) : ℕ

First unused absolute wire after this build and its primary-input prefix.

Equations

• build.available primaryAvailable = primaryAvailable + List.length build.circuit

def Complexity.CircuitUnrolling.initialAcceptanceCopiesBuild (runs : ℕ) : AcceptanceCopiesBuild runs

Empty acceptance-copy build. Verdict entries are placeholders until their corresponding runs are emitted.

Equations

• Complexity.CircuitUnrolling.initialAcceptanceCopiesBuild runs = { circuit := [], verdictWires := fun (x : Fin runs) => 0 }

noncomputable def Complexity.CircuitUnrolling.acceptanceCopiesBuildStep {k : ℕ} (tm : NTM k) {runs T n primaryAvailable : ℕ} (layout : ParallelInputWires runs T n primaryAvailable) (build : AcceptanceCopiesBuild runs) (j : Fin runs) : AcceptanceCopiesBuild runs

Append one bounded-trace acceptance circuit and record its final wire as the selected run's verdict. The run layout is weakened across all gates emitted by earlier copies without changing any primary-input index.

Equations

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

noncomputable def Complexity.CircuitUnrolling.acceptanceCopiesBuildFrom {k : ℕ} (tm : NTM k) {runs T n primaryAvailable : ℕ} (layout : ParallelInputWires runs T n primaryAvailable) (build : AcceptanceCopiesBuild runs) (indices : List (Fin runs)) : AcceptanceCopiesBuild runs

Append a listed sequence of acceptance copies to an existing build.

Equations

• Complexity.CircuitUnrolling.acceptanceCopiesBuildFrom tm layout build indices = List.foldl (Complexity.CircuitUnrolling.acceptanceCopiesBuildStep tm layout) build indices

noncomputable def Complexity.CircuitUnrolling.prefixAcceptanceCopiesBuild {k : ℕ} (tm : NTM k) (runs T n primaryAvailable i : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : AcceptanceCopiesBuild runs

Build the first i canonical acceptance copies. List take saturates when i exceeds the total number of runs.

Equations

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

noncomputable def Complexity.CircuitUnrolling.acceptanceCopiesBuild {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : AcceptanceCopiesBuild runs

Complete build containing one independent acceptance circuit per run.

Equations

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

noncomputable def Complexity.CircuitUnrolling.acceptanceCopiesFragment {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : CircuitCode.RawCircuit

Raw concatenation of every independent acceptance copy.

Equations

• Complexity.CircuitUnrolling.acceptanceCopiesFragment tm runs T n primaryAvailable layout = (Complexity.CircuitUnrolling.acceptanceCopiesBuild tm runs T n primaryAvailable layout).circuit

noncomputable def Complexity.CircuitUnrolling.acceptanceCopiesSize {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : ℕ

Exact gate count recorded after emitting every acceptance copy.

Equations

• Complexity.CircuitUnrolling.acceptanceCopiesSize tm runs T n primaryAvailable layout = List.length (Complexity.CircuitUnrolling.acceptanceCopiesBuild tm runs T n primaryAvailable layout).circuit

noncomputable def Complexity.CircuitUnrolling.acceptanceCopiesVerdictWires {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : Fin runs → ℕ

Absolute wire carrying each run's acceptance verdict.

Equations

• Complexity.CircuitUnrolling.acceptanceCopiesVerdictWires tm runs T n primaryAvailable layout = (Complexity.CircuitUnrolling.acceptanceCopiesBuild tm runs T n primaryAvailable layout).verdictWires

def Complexity.CircuitUnrolling.strictMajorityThreshold (runs : ℕ) : ℕ

Smallest integer count constituting a strict majority of runs.

Equations

• Complexity.CircuitUnrolling.strictMajorityThreshold runs = runs / 2 + 1

def Complexity.CircuitUnrolling.parallelAcceptanceBits {k n runs : ℕ} (tm : NTM k) (T : ℕ) (x : BitString n) (choices : Fin runs → BitString T) : BitString runs

Acceptance bits produced by independent bounded runs sharing one input.

Equations

• Complexity.CircuitUnrolling.parallelAcceptanceBits tm T x choices j = Complexity.CircuitUnrolling.boundedAcceptanceBit tm T x (choices j)

def Complexity.CircuitUnrolling.parallelChoiceBlocks (runs T : ℕ) (seed : BitString (runs * T)) : Fin runs → BitString T

Split a flat row-major seed into one bounded choice block per run.

Equations

• Complexity.CircuitUnrolling.parallelChoiceBlocks runs T seed j t = seed (finProdFinEquiv (j, t))

@[simp]

theorem Complexity.CircuitUnrolling.parallelChoiceBlocks_apply (runs T : ℕ) (seed : BitString (runs * T)) (j : Fin runs) (t : Fin T) : parallelChoiceBlocks runs T seed j t = seed (finProdFinEquiv (j, t))

Reading a flat seed's (j, t) entry uses the canonical product index.

def Complexity.CircuitUnrolling.canonicalAcceptanceBits {k n : ℕ} (tm : NTM k) (runs T : ℕ) (x : BitString n) (seed : BitString (runs * T)) : BitString runs

Per-run acceptance bits under the canonical flattened-seed layout.

Equations

• Complexity.CircuitUnrolling.canonicalAcceptanceBits tm runs T x seed = Complexity.CircuitUnrolling.parallelAcceptanceBits tm T x (Complexity.CircuitUnrolling.parallelChoiceBlocks runs T seed)

noncomputable def Complexity.CircuitUnrolling.amplifiedAcceptanceRawCircuit {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : CircuitCode.RawCircuit

Independent bounded-trace acceptance copies followed by a strict-majority threshold over their recorded verdict wires.

Equations

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

noncomputable def Complexity.CircuitUnrolling.amplifiedAcceptanceOutputWire {k : ℕ} (tm : NTM k) (runs T n primaryAvailable : ℕ) (layout : ParallelInputWires runs T n primaryAvailable) : ℕ

Absolute wire carrying the amplified circuit's strict-majority output.

Equations

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

noncomputable def Complexity.CircuitUnrolling.canonicalAmplifiedAcceptanceRawCircuit {k : ℕ} (tm : NTM k) (runs T n : ℕ) : CircuitCode.RawCircuit

Canonical amplified raw circuit with all flattened choice blocks before the shared input data.

Equations

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