P/poly and circuit-size classes

This module supplies the public API for nonuniform circuit classes. It relates the exact pointwise-polynomial definition of PPoly to the big-O power convention used elsewhere in the library.

@[simp]

theorem Complexity.BoolFunFamily.mem_toLanguage {f : BoolFunFamily} {x : List Bool} : x ∈ f.toLanguage ↔ f x.length x.get = true

A list belongs to the language of a Boolean function family iff the length-indexed function evaluates to true on its entries.

theorem Complexity.BoolFunFamily.mem_toLanguage_toList {f : BoolFunFamily} {n : ℕ} (x : BitString n) : x.toList ∈ f.toLanguage ↔ f n x = true

The serialization of a length-n bitstring lies in f.toLanguage iff f n evaluates to true on that bitstring.

theorem Complexity.BoolFunFamily.toLanguage_injective : Function.Injective toLanguage

Distinct Boolean function families induce distinct languages: toLanguage is injective.

@[simp]

theorem Complexity.CircuitFamily.mem_language {B : Basis} {F : CircuitFamily B} {x : List Bool} : x ∈ F.language ↔ F.evalList x = true

A list belongs to the language of a circuit family iff the circuit for its length evaluates to true on it.

theorem Complexity.CircuitFamily.nil_mem_language {B : Basis} {F : CircuitFamily B} : [] ∈ F.language ↔ F.emptyOutput = true

The empty string is in a circuit family's language iff the length-zero circuit outputs true.

theorem Complexity.CircuitFamily.decides_iff {B : Basis} (F : CircuitFamily B) (L : Language) : F.Decides L ↔ ∀ (x : List Bool), F.evalList x = true ↔ x ∈ L

A circuit family decides L iff its list-level evaluation agrees with membership in L on every input.

theorem Complexity.CircuitFamily.decides_congr {B : Basis} (F : CircuitFamily B) {L K : Language} (h : L = K) : F.Decides L ↔ F.Decides K

Decides respects equality of languages: deciding L and deciding K are equivalent when L = K.

theorem Complexity.CircuitFamily.decides_unique {B : Basis} (F : CircuitFamily B) {L K : Language} (hL : F.Decides L) (hK : F.Decides K) : L = K

A circuit family decides at most one language: if F decides both L and K, then L = K.

theorem Complexity.CircuitFamily.Decides.evalList {B : Basis} {F : CircuitFamily B} {L : Language} (h : F.Decides L) (x : List Bool) : F.evalList x = true ↔ x ∈ L

If F decides L, then its list-level evaluation returns true exactly on members of L.

theorem Complexity.CircuitFamily.Decides.apply {B : Basis} {F : CircuitFamily B} {L : Language} (h : F.Decides L) {n : ℕ} (x : BitString n) : F.function n x = true ↔ x.toList ∈ L

A deciding family agrees with language membership on the canonical serialization of every fixed-length input.

theorem Complexity.CircuitFamily.Computes.decides {B : Basis} {F : CircuitFamily B} {f : BoolFunFamily} (h : F.Computes f) : F.Decides f.toLanguage

A circuit family computing a Boolean function family decides the language induced by that family.

theorem Complexity.CircuitFamily.decides_toLanguage_iff {B : Basis} (F : CircuitFamily B) (f : BoolFunFamily) : F.Decides f.toLanguage ↔ F.Computes f

Computing a Boolean function family is equivalent to deciding its induced language.

theorem Complexity.SIZEWithBasis_mono (B : Basis) {s t : ℕ → ℕ} (hst : ∀ (n : ℕ), s n ≤ t n) : SIZEWithBasis B s ⊆ SIZEWithBasis B t

SIZEWithBasis B is monotone: pointwise enlarging the size bound only enlarges the class.

theorem Complexity.SIZE_mono {s t : ℕ → ℕ} (hst : ∀ (n : ℕ), s n ≤ t n) : SIZE s ⊆ SIZE t

SIZE is monotone: pointwise enlarging the size bound only enlarges the class.

theorem Complexity.mem_PPoly_iff {L : Language} : L ∈ PPoly ↔ ∃ (F : CircuitFamily Basis.andOr2) (k : ℕ), F.Decides L ∧ BigO F.size fun (x : ℕ) => x ^ k

Big-O characterization of membership in PPoly.

theorem Complexity.PPoly_eq_iUnion_SIZE : PPoly = ⋃ (p : Polynomial ℕ), SIZE fun (n : ℕ) => Polynomial.eval n p

PPoly is definitionally the union of the pointwise SIZE classes over all natural-coefficient polynomials. This is not the substantive advice-machine characterization of P/poly.