Polynomial-size circuit oracles -- definitions

This module packages a language-deciding circuit family together with a polynomial asymptotic size certificate. Its induced Boolean oracle evaluates the family member selected by the query length.

structure Complexity.PolynomialCircuitOracle (language : Language) : Type

A polynomial-size fan-in-two AND/OR circuit family deciding language.

The exponent is stored explicitly so downstream circuit-inlining arguments can track the size of the oracle circuit used at each fixed query width.

• family : CircuitFamily Basis.andOr2

  The circuit family supplying one Boolean oracle circuit per query width.

• exponent : ℕ

  Exponent in the family's polynomial asymptotic size bound.

• decides : self.family.Decides language

  Exact agreement between the family and the oracle language.

• size_bigO : BigO self.family.size fun (x : ℕ) => x ^ self.exponent

  Polynomial asymptotic size of the circuit family.

def Complexity.PolynomialCircuitOracle.oracle {language : Language} (circuitOracle : PolynomialCircuitOracle language) : BooleanOracle

The Boolean oracle induced by evaluating the length-indexed circuit family on each query.

Equations

• circuitOracle.oracle = circuitOracle.family.evalList