SAT circuit oracles from NP ⊆ P/poly

This module extracts the exact polynomial-size SAT circuit family needed to replace SAT-oracle calls in a nonuniform computation. Fixed-round adaptive programs may have a different positive query width at each round; the selected family members inline every call into one ordinary circuit.

theorem Complexity.SAT.exists_polynomialCircuitOracle_of_NP_subset_PPoly (hNP : NP ⊆ PPoly) : Nonempty (PolynomialCircuitOracle language)

If every language in NP has polynomial-size circuits, then SAT has a packaged polynomial-size circuit oracle.

theorem Complexity.SAT.exists_inlinedCircuitOracle_of_NP_subset_PPoly (hNP : NP ⊆ PPoly) {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) : ∃ (circuitOracle : PolynomialCircuitOracle language), circuitOracle.oracle.Decides language ∧ ∀ (input : BitString inputWidth), (program.inlineCircuitOracle circuitOracle).snd.eval input = program.eval circuitOracle.oracle input

Under NP ⊆ PPoly, every fixed-round adaptive SAT-oracle circuit program has a polynomial circuit oracle whose width-selected family members inline to an ordinary circuit with exactly the same output.

This theorem performs circuit-level oracle replacement. It does not assert that an arbitrary oracle Turing machine has already been compiled into an AdaptiveOracleProgram.