Inlining polynomial circuit oracles -- proof internals

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

Internal proof that the width-selected family members implement the induced Boolean oracle in every round.

theorem Complexity.PolynomialCircuitOracle.implementation_circuit_size_internal {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)

Internal size identity for each width-selected oracle circuit.

theorem Complexity.AdaptiveOracleProgram.inlineCircuitOracle_eval_internal {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

Internal semantic correctness of inlining a polynomial circuit oracle.

theorem Complexity.AdaptiveOracleProgram.inlineCircuitOracle_size_internal {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

Internal exact size of a circuit with every oracle call inlined.