Documentation

Complexitylib.Circuits.Unrolling.Acceptance.Hardwiring

Fixed-choice bounded acceptance circuits #

This module fixes the choices-first prefix of a canonical bounded acceptance circuit, leaving only the positive-length data input live. It is the reusable single-run analogue of amplified-seed hardwiring.

Main definitions and results #

source
noncomputable def Complexity.CircuitUnrolling.fixedChoicesAcceptanceCircuit {k : ℕ} (tm : NTM k) (T n : ℕ) [NeZero n] (choices : BitString T) :
Circuit Basis.andOr2 n 1 (List.length (acceptanceRawCircuit tm T n (T + n) (prefixInputWires T n)) - 1)

Fix every choice input of a canonical bounded acceptance circuit while leaving its positive-length data suffix live.

Equations
Instances For
    source
    theorem Complexity.CircuitUnrolling.fixedChoicesAcceptanceCircuit_eval {k : ℕ} (tm : NTM k) (T n : ℕ) [NeZero n] (choices : BitString T) (x : BitString n) :
    (fixedChoicesAcceptanceCircuit tm T n choices).eval x 0 = boundedAcceptanceBit tm T x choices

    Fixing the choice prefix preserves the exact bounded acceptance bit.

    source
    @[simp]
    theorem Complexity.CircuitUnrolling.fixedChoicesAcceptanceCircuit_size {k : ℕ} (tm : NTM k) (T n : ℕ) [NeZero n] (choices : BitString T) :
    (fixedChoicesAcceptanceCircuit tm T n choices).size = (canonicalAcceptanceCircuit tm T n).size

    Fixing the choice prefix preserves the canonical circuit's exact size.

    source
    theorem Complexity.CircuitUnrolling.fixedChoicesAcceptanceCircuit_size_le {k : ℕ} (tm : NTM k) (T n : ℕ) [NeZero n] (choices : BitString T) :
    (fixedChoicesAcceptanceCircuit tm T n choices).size ≤ acceptanceSizeCoeff tm * (T + 2) ^ 3

    A fixed-choice acceptance circuit inherits the canonical cubic bound.