Nonuniform circuits as polynomial advice

This module exposes the reverse half of the advice/circuit characterization. The canonical serialized member of a polynomial-size circuit family is used as length-dependent advice for the verified circuit evaluator.

Main results

• CircuitFamily.polynomialAdvice_encodeAt: canonical family codes have polynomial length for polynomial-size families.
• CircuitFamily.Decides.evalFamilyTM_decidesWithAdviceInTime: the verified evaluator decides the family's language from those codes.
• CircuitFamily.Decides.mem_PAdvice: package one polynomial-size deciding family as a polynomial-advice decider.
• PPoly_subset_PAdvice: P/poly is contained in polynomial advice.

theorem Complexity.CircuitFamily.polynomialAdvice_encodeAt (F : CircuitFamily Basis.andOr2) {d : ℕ} (hsize : BigO F.size fun (x : ℕ) => x ^ d) : PolynomialAdvice F.encodeAt

Canonical member encodings of a polynomial-size family form polynomial-length advice.

theorem Complexity.CircuitFamily.Decides.evalFamilyTM_decidesWithAdviceInTime {F : CircuitFamily Basis.andOr2} {L : Language} (hdec : F.Decides L) : CircuitCode.Machine.evalFamilyTM.DecidesWithAdviceInTime F.encodeAt L F.adviceEvalTime

The verified serialized evaluator decides a circuit family's language when the canonical member code is supplied as advice.

theorem Complexity.CircuitFamily.adviceEvalTime_bigO (F : CircuitFamily Basis.andOr2) {d : ℕ} (hsize : BigO F.size fun (x : ℕ) => x ^ d) : BigO F.adviceEvalTime fun (x : ℕ) => x ^ (4 * (d + 1))

Evaluating the canonical member-code advice of a size-O(n^d) family runs in time O(n^(4(d+1))), measured in the original input length.

theorem Complexity.CircuitFamily.Decides.mem_PAdvice {F : CircuitFamily Basis.andOr2} {L : Language} {d : ℕ} (hdec : F.Decides L) (hsize : BigO F.size fun (x : ℕ) => x ^ d) : L ∈ PAdvice

A polynomial-size circuit family deciding L directly witnesses L ∈ PAdvice through the verified serialized evaluator.

theorem Complexity.PPoly_subset_PAdvice : PPoly ⊆ PAdvice

Polynomial-size nonuniform circuits can be evaluated in polynomial time when their canonical member encodings are supplied as advice.