Inlining polynomial circuit oracles

This module turns a fixed-round adaptive computation relative to any language in P/poly into an ordinary circuit by selecting and inlining the relevant query-width circuit-family members.

theorem Complexity.PolynomialCircuitOracle.implementation_implements {language : Language} (circuitOracle : PolynomialCircuitOracle language) {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) : (circuitOracle.implementation program).Implements circuitOracle.oracle

The width-selected family members implement the circuit oracle's induced Boolean oracle in every adaptive round.

@[simp]

theorem Complexity.PolynomialCircuitOracle.implementation_circuit_size {language : Language} (circuitOracle : PolynomialCircuitOracle language) {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (round : Fin rounds) : ((circuitOracle.implementation program).circuit round).size = circuitOracle.family.size (program.queryWidth round)

Each selected oracle circuit has exactly the circuit-family size at that round's query width.

theorem Complexity.AdaptiveOracleProgram.inlineCircuitOracle_eval {language : Language} {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (circuitOracle : PolynomialCircuitOracle language) (input : BitString inputWidth) : (program.inlineCircuitOracle circuitOracle).snd.eval input = program.eval circuitOracle.oracle input

Replacing all adaptive oracle calls by their polynomial circuit-family members preserves the program output on every input.

theorem Complexity.AdaptiveOracleProgram.inlineCircuitOracle_size {language : Language} {inputWidth outputWidth rounds : ℕ} [NeZero inputWidth] [NeZero outputWidth] (program : AdaptiveOracleProgram inputWidth outputWidth rounds) (circuitOracle : PolynomialCircuitOracle language) : (program.inlineCircuitOracle circuitOracle).snd.size = program.inlineHistorySize (circuitOracle.implementation program) rounds ⋯ + program.final.size

The ordinary inlined circuit has exactly the adaptive-history recurrence plus the final output circuit's size.