P ⊆ P/poly and BPP ⊆ P/poly

A problem decided in polynomial time has circuits of polynomial size Arora and Barak, Theorem 6.6: the machine deciding it writes [true] within polynomially many steps exactly on the encoded members, and the inputs on which a machine does so form a language in P/poly (MachineSimulation.acceptedWithin_mem_PPoly). With Adleman's theorem (PPoly.of_boundedError), the same holds for problems decided with bounded error Arora and Barak, Theorem 7.14: the verifier's circuits read frame x ++ r, whose bits are bits of x, bits of r or constants (frameWiring), so they are circuits for a function of x ++ r of the same size up to two gates.

Main results

• Cslib.Circuits.Boolean.PPoly.exists_of_polyTime: the instances on which a Boolean function computable in polynomial time is true are the preimage of a language in P/poly.
• Cslib.Circuits.Boolean.PPoly.exists_of_mem_P: a problem in P, with any encoding of its instances, is the preimage of a language in P/poly.
• Cslib.Circuits.Boolean.PPoly.of_mem_P: P ⊆ P/poly for languages over Bool.
• Cslib.Circuits.Boolean.PPoly.exists_of_mem_BPP, PPoly.exists_of_mem_RP: the same for BPP and RP, with any encoding.
• Cslib.Circuits.Boolean.PPoly.of_mem_BPP, PPoly.of_mem_RP, PPoly.of_mem_coRP: BPP, RP, coRP ⊆ P/poly for languages over Bool.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 7.5
• M. Sipser, Introduction to the Theory of Computation, Section 9.3

theorem Cslib.Circuits.Boolean.PPoly.exists_of_polyTime {α : Type u_1} {enc : α ↪ List Bool} {f : α → Bool} (hf : Turing.MultiTapeTM.ComputableInPolyTime f enc Turing.MultiTapeTM.encBool) : ∃ L ∈ PPoly, ∀ (a : α), f a = true ↔ enc a ∈ L

The instances on which a Boolean function computable in polynomial time is true are the preimage, under the encoding, of a language in P/poly.

theorem Cslib.Circuits.Boolean.PPoly.exists_of_mem_P {α : Type u_1} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ Complexity.P enc) : ∃ L ∈ PPoly, ∀ (a : α), a ∈ A ↔ enc a ∈ L

P ⊆ P/poly. A problem in P, with any encoding enc of its instances, is the preimage under enc of a language in P/poly.

theorem Cslib.Circuits.Boolean.PPoly.of_mem_P {L : Language Bool} (hL : L ∈ Complexity.P Turing.MultiTapeTM.encBits) : L ∈ PPoly

P ⊆ P/poly for languages over Bool, with words encoded as themselves.

Randomised classes

def Cslib.Circuits.Boolean.frameWiring (n P : ℕ) (j : Fin (2 * n + 1 + P)) : Fin (n + P) ⊕ Bool

The substitution feeding a function of 2 n + 1 + P variables with frame x ++ r, from the variables x ++ r.

theorem Cslib.Circuits.Boolean.ofFn_substitute_frameWiring {n P : ℕ} (x : Fin n → Bool) (r : Fin P → Bool) : List.ofFn (substitute (frameWiring n P) (Fin.append x r)) = Turing.MultiTapeTM.frame (List.ofFn x) ++ List.ofFn r

noncomputable def Cslib.Circuits.Boolean.framedSlice (L : Language Bool) (n P : ℕ) : BooleanFunction (n + P)

The function of x ++ r that tests frame x ++ r ∈ L.

theorem Cslib.Circuits.Boolean.framedSlice_append_eq_true {L : Language Bool} {n P : ℕ} (x : Fin n → Bool) (r : Fin P → Bool) : framedSlice L n P (Fin.append x r) = true ↔ Turing.MultiTapeTM.frame (List.ofFn x) ++ List.ofFn r ∈ L

theorem Cslib.Circuits.Boolean.polynomiallyBounded_complexity_framedSlice {L : Language Bool} (hL : L ∈ PPoly) {p : ℕ → ℕ} (hp : PolynomiallyBounded p) : PolynomiallyBounded fun (n : ℕ) => complexity interpretation (single (framedSlice L n (p n)))

Framing costs at most two gates.

def Cslib.Circuits.Boolean.encodes {α : Type} (enc : α ↪ List Bool) (n : ℕ) : Set (Fin n → Bool)

The words of length n that encode an instance.

noncomputable def Cslib.Circuits.Boolean.encodesMember {α : Type} (enc : α ↪ List Bool) (A : Set α) (n : ℕ) : BooleanFunction n

Whether the word x encodes a member of A.

theorem Cslib.Circuits.Boolean.encodesMember_eq_true_iff {α : Type} {enc : α ↪ List Bool} {A : Set α} {n : ℕ} {x : Fin n → Bool} {a : α} (ha : enc a = List.ofFn x) : encodesMember enc A n x = true ↔ a ∈ A

theorem Cslib.Circuits.Boolean.mem_iff_of_slice_eq_encodesMember {α : Type} {enc : α ↪ List Bool} {L : Language Bool} {A : Set α} (h : ∀ (n : ℕ), ∀ x ∈ encodes enc n, L.slice n x = encodesMember enc A n x) (a : α) : a ∈ A ↔ enc a ∈ L

A language agreeing with encodesMember enc A on encoded words contains exactly the encodings of the members of A.

theorem Cslib.Circuits.Boolean.verifier_eq_true_iff {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} {L : Language Bool} (hVL : ∀ (y : α × List Bool), V y = true ↔ (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) y ∈ L) {n : ℕ} {x : Fin n → Bool} {a : α} (ha : enc a = List.ofFn x) (r : List Bool) {P : ℕ} (r' : Fin P → Bool) (hr : r = List.ofFn r') : V (a, r) = true ↔ framedSlice L n P (Fin.append x r') = true

The verifier on an encoded instance, as the framed slice of the language deciding it.

theorem Cslib.Circuits.Boolean.PPoly.exists_of_mem_BPP {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ Complexity.BPP enc) : ∃ L ∈ PPoly, ∀ (a : α), a ∈ A ↔ enc a ∈ L

BPP ⊆ P/poly. A problem in BPP, with any encoding enc of its instances, is the preimage under enc of a language in P/poly.

theorem Cslib.Circuits.Boolean.PPoly.exists_of_mem_RP {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ Complexity.RP enc) : ∃ L ∈ PPoly, ∀ (a : α), a ∈ A ↔ enc a ∈ L

RP ⊆ P/poly. A problem in RP, with any encoding enc of its instances, is the preimage under enc of a language in P/poly.

theorem Cslib.Circuits.Boolean.PPoly.of_mem_BPP {A : Language Bool} (hA : A ∈ Complexity.BPP Turing.MultiTapeTM.encBits) : A ∈ PPoly

BPP ⊆ P/poly for languages over Bool, with words encoded as themselves.

theorem Cslib.Circuits.Boolean.PPoly.of_mem_RP {A : Language Bool} (hA : A ∈ Complexity.RP Turing.MultiTapeTM.encBits) : A ∈ PPoly

RP ⊆ P/poly for languages over Bool, with words encoded as themselves.

theorem Cslib.Circuits.Boolean.PPoly.of_mem_coRP {A : Language Bool} (hA : A ∈ Complexity.coRP Turing.MultiTapeTM.encBits) : A ∈ PPoly

coRP ⊆ P/poly for languages over Bool.