Polynomial advice and nonuniform circuits

This module exposes the polynomial-advice machine class and its equivalence with polynomial-size nonuniform circuits. The reverse simulation supplies each canonical family-member encoding as advice to the verified serialized-circuit evaluator.

Main definitions and results

• Advice, advisedInput, PolynomialAdvice: the advice convention.
• TM.DecidesWithAdviceInTime, PAdvice: advised decision and its class.
• TM.adviceCircuitFamily: hardwire advice into bounded acceptance circuits.
• PAdvice_subset_PPoly: polynomial-time advice machines have polynomial-size circuit families.
• PPoly_subset_PAdvice: polynomial-size circuit families yield polynomial-time advice machines.
• PAdvice_eq_PPoly: the two nonuniform formulations coincide.

@[simp]

theorem Complexity.advisedInput_length (a : Advice) (x : List Bool) : (advisedInput a x).length = 2 * (a x.length).length + 2 + x.length

The advised input has the exact self-delimiting pairing length.

theorem Complexity.Advice.fixedPrefix_append (a : Advice) (x : List Bool) : a.fixedPrefix x.length ++ x = advisedInput a x

The fixed advice prefix followed by x is exactly the advised machine input.

@[simp]

theorem Complexity.Advice.inputBits_toList (a : Advice) {n : ℕ} (x : BitString n) : (a.inputBits x).toList = advisedInput a x.toList

The fixed-prefix bit string serializes to the self-delimiting advised machine input.

theorem Complexity.Advice.polynomialAdvice_iff_bigO (a : Advice) : PolynomialAdvice a ↔ ∃ (d : ℕ), BigO (fun (n : ℕ) => (a n).length) fun (x : ℕ) => x ^ d

Advice has polynomial length exactly when its length function has a big-O power bound.

theorem Complexity.Advice.polynomialAdvice_nil : PolynomialAdvice fun (x : ℕ) => []

Empty advice has constant (hence polynomial) length.

theorem Complexity.PolynomialAdvice.of_length_le {a b : Advice} (hb : PolynomialAdvice b) (hle : ∀ (n : ℕ), (a n).length ≤ (b n).length) : PolynomialAdvice a

Pointwise shortening preserves polynomial advice length.

theorem Complexity.TM.DecidesWithAdviceInTime.mono {k : ℕ} {tm : TM k} {a : Advice} {L : Language} {T T' : ℕ → ℕ} (hle : ∀ (n : ℕ), T n ≤ T' n) (hdec : tm.DecidesWithAdviceInTime a L T) : tm.DecidesWithAdviceInTime a L T'

Advised decision is monotone under pointwise enlargement of its time bound.

theorem Complexity.TM.DecidesWithAdviceInTime.advisedBoundedAcceptanceBit_iff {k : ℕ} {tm : TM k} {a : Advice} {L : Language} {T : ℕ → ℕ} (hdec : tm.DecidesWithAdviceInTime a L T) (n : ℕ) (x : BitString n) : tm.advisedBoundedAcceptanceBit a T x = true ↔ x.toList ∈ L

Exact-horizon advised acceptance agrees with ordinary language membership.

theorem Complexity.TM.adviceCircuitFamily_function {k : ℕ} (tm : TM k) (a : Advice) (T : ℕ → ℕ) (n : ℕ) (x : BitString n) : (tm.adviceCircuitFamily a T).function n x = tm.advisedBoundedAcceptanceBit a T x

The hardwired advice family computes the exact bounded advised verdict.

theorem Complexity.TM.DecidesWithAdviceInTime.adviceCircuitFamily_decides {k : ℕ} {tm : TM k} {a : Advice} {L : Language} {T : ℕ → ℕ} (hdec : tm.DecidesWithAdviceInTime a L T) : (tm.adviceCircuitFamily a T).Decides L

The hardwired advice family decides the advised machine's language.

theorem Complexity.TM.adviceCircuitFamily_size_le {k : ℕ} (tm : TM k) (a : Advice) (T : ℕ → ℕ) (n : ℕ) : (tm.adviceCircuitFamily a T).size n ≤ CircuitUnrolling.acceptanceSizeCoeff tm.toNTM * (T n + 2) ^ 3

Pointwise cubic size bound for hardwired advised computation.

theorem Complexity.TM.adviceCircuitFamily_size_bigO {k : ℕ} (tm : TM k) (a : Advice) {T : ℕ → ℕ} {d : ℕ} (hT : BigO T fun (x : ℕ) => x ^ d) : BigO (tm.adviceCircuitFamily a T).size fun (x : ℕ) => x ^ (3 * d)

A time-O(n^d) advised computation yields a circuit family of size O(n^(3d)).

theorem Complexity.TM.DecidesWithAdviceInTime.mem_PPoly {k : ℕ} {tm : TM k} {a : Advice} {L : Language} {T : ℕ → ℕ} {d : ℕ} (hdec : tm.DecidesWithAdviceInTime a L T) (hT : BigO T fun (x : ℕ) => x ^ d) : L ∈ PPoly

One polynomial-time advised decider directly witnesses membership in P/poly.

No advice-length hypothesis is needed for this direction: the advice prefix is hardwired without adding gates, while the unrolling size depends only on the time horizon. PAdvice still requires polynomial advice length to match the standard class convention.

theorem Complexity.PAdvice_subset_PPoly : PAdvice ⊆ PPoly

Polynomial-time advice machines have polynomial-size nonuniform circuits.

theorem Complexity.PAdvice_eq_PPoly : PAdvice = PPoly

Polynomial advice and polynomial-size nonuniform circuit families define the same language class.