Nonuniform circuits as polynomial advice — proof internals

This module supplies a circuit family member's canonical code as advice to the verified serialized evaluator. It proves polynomial advice length, evaluator correctness on that advice, and polynomial time measured in the original input length.

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

Internal proof that canonical member encodings of a polynomial-size family form polynomial-length advice.

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

Internal correctness of the serialized evaluator when F.encodeAt is used as its length-dependent advice.

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

Internal polynomial bound for evaluating the canonical member-code advice of a polynomial-size circuit family.

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

Internal packaging of one polynomial-size deciding circuit family as a polynomial-time advised evaluator.

theorem Complexity.PPoly_subset_PAdvice_internal : PPoly ⊆ PAdvice

Internal proof that polynomial-size nonuniform circuits can be evaluated in polynomial time using their canonical member codes as advice.