Polynomial-size circuit oracles

This module identifies P/poly membership with the existence of a packaged polynomial-size circuit oracle and proves that the induced Boolean oracle has the intended exact language semantics.

theorem Complexity.PolynomialCircuitOracle.oracle_decides {language : Language} (circuitOracle : PolynomialCircuitOracle language) : circuitOracle.oracle.Decides language

Evaluating the packaged circuit family gives an exact oracle for its language.

theorem Complexity.PolynomialCircuitOracle.circuit_eval_eq_oracle {language : Language} (circuitOracle : PolynomialCircuitOracle language) {queryWidth : ℕ} [NeZero queryWidth] (query : BitString queryWidth) : (circuitOracle.family.circuit queryWidth).eval query 0 = circuitOracle.oracle query.toList

At every positive query width, the selected family member computes the induced Boolean oracle on the serialized query.

theorem Complexity.PolynomialCircuitOracle.circuit_size_eq_family_size {language : Language} (circuitOracle : PolynomialCircuitOracle language) (queryWidth : ℕ) [NeZero queryWidth] : (circuitOracle.family.circuit queryWidth).size = circuitOracle.family.size queryWidth

At every positive width, the selected oracle circuit's size is the circuit family's size at that width.

theorem Complexity.mem_PPoly_iff_nonempty_polynomialCircuitOracle {language : Language} : language ∈ PPoly ↔ Nonempty (PolynomialCircuitOracle language)

A language is in P/poly exactly when it has a packaged polynomial-size circuit oracle.