Polynomial advice — proof internals

This module proves representation laws, exact semantics, and polynomial size for advised-computation circuit families. Public statements are exposed by Complexitylib.Classes.PPoly.Advice.

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

Internal serialization law for the fixed-prefix advised input.

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

Internal big-O characterization of polynomial advice length.

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

Internal monotonicity of polynomial advice under pointwise shortening.

theorem Complexity.TM.DecidesWithAdviceInTime.mono_internal {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'

Internal time-bound monotonicity for advised decision.

theorem Complexity.TM.DecidesWithAdviceInTime.advisedBoundedAcceptanceBit_iff_internal {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

Internal exact-horizon correctness of the advised bounded acceptance bit.

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

Internal semantics of the hardwired advice circuit family.

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

Internal whole-language correctness of the hardwired advice family.

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

Internal pointwise cubic size bound for the hardwired advice family.

theorem Complexity.TM.adviceCircuitFamily_size_bigO_internal {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)

Internal asymptotic size bound for the hardwired advice family.

theorem Complexity.TM.DecidesWithAdviceInTime.mem_PPoly_internal {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

Internal packaging theorem from one polynomial-time advised decider to P/poly.

theorem Complexity.PAdvice_subset_PPoly_internal : PAdvice ⊆ PPoly

Internal proof that polynomial-time advice machines have polynomial-size nonuniform circuits.