Probabilistic semantics of circuit amplification

This module is the dependency boundary between circuit unrolling and finite probability. The circuit layer counts true verdict wires with Fin.countP; the randomized-complexity layer interprets the same vector as independent choice blocks and hence as blockEventCount and blockMajority. It also provides the fixed-seed wrapper that hardwires every choice input while leaving the positive-length data suffix live.

theorem Complexity.CircuitUnrolling.finCountP_canonicalAcceptanceBits_eq_blockEventCount {k n : ℕ} (tm : NTM k) (runs T : ℕ) (x : BitString n) (seed : BitString (runs * T)) : Fin.countP (canonicalAcceptanceBits tm runs T x seed) = blockEventCount (tm.repeatAcceptEvent x.toList T) seed

Counting canonical circuit verdicts is exactly counting accepting blocks in the compact repetition seed.

theorem Complexity.CircuitUnrolling.canonicalThresholdValue_eq_blockMajority {k n : ℕ} (tm : NTM k) (runs T : ℕ) (x : BitString n) (seed : BitString (runs * T)) : decide (strictMajorityThreshold runs ≤ Fin.countP (canonicalAcceptanceBits tm runs T x seed)) = blockMajority (tm.repeatAcceptEvent x.toList T) seed

The circuit encoder's at-least threshold is the randomized layer's strict block-majority predicate.

theorem Complexity.CircuitUnrolling.canonicalAmplifiedAcceptanceCircuit_eval_eq_blockMajority {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 = blockMajority (tm.repeatAcceptEvent x.toList T) seed

The canonical typed amplification circuit computes exactly the compact seed's block-majority acceptance predicate.

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

Fix every random-choice input of a canonical amplified acceptance circuit, leaving only the positive-length data input live. This is the generic circuit-level bridge from an amplified random seed to nonuniform advice.

Equations

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

theorem Complexity.CircuitUnrolling.fixedSeedAmplifiedAcceptanceCircuit_eval {k : ℕ} (tm : NTM k) (runs T n : ℕ) [NeZero n] (seed : BitString (runs * T)) (x : BitString n) : (fixedSeedAmplifiedAcceptanceCircuit tm runs T n seed).eval x 0 = blockMajority (tm.repeatAcceptEvent x.toList T) seed

A fixed-seed amplified circuit computes the block-majority verdict for that seed and the live data input.

@[simp]

theorem Complexity.CircuitUnrolling.fixedSeedAmplifiedAcceptanceCircuit_size {k : ℕ} (tm : NTM k) (runs T n : ℕ) [NeZero n] (seed : BitString (runs * T)) : (fixedSeedAmplifiedAcceptanceCircuit tm runs T n seed).size = (canonicalAmplifiedAcceptanceCircuit tm runs T n).size

Fixing the random seed preserves the amplified circuit's exact size.

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

A fixed-seed amplified circuit inherits the canonical cubic-by-quadratic size bound.