Oracle programs for relative approximate counting -- proof internals

theorem Complexity.ApproximateCounting.Relative.inlineCircuitImplements_internal {inputWidth outputWidth domainWidth rounds precision failureBits : ℕ} [NeZero inputWidth] [NeZero outputWidth] {setOfInput : BitString inputWidth → Finset (BitString domainWidth)} {program : AdaptiveOracleProgram (seedWidth domainWidth precision failureBits + inputWidth) outputWidth rounds} {oracle : BooleanOracle} (implementation : program.OracleCircuitImplementation) (himplementation : implementation.Implements oracle) (hprogram : OracleProgramImplements precision failureBits setOfInput program oracle) : CircuitImplements precision failureBits setOfInput (program.inline implementation).snd

theorem Complexity.ApproximateCounting.Relative.exists_hardwired_accurate_of_mem_PPoly_internal {language : Language} {inputWidth outputWidth domainWidth rounds precision : ℕ} [NeZero inputWidth] [NeZero outputWidth] {setOfInput : BitString inputWidth → Finset (BitString domainWidth)} (program : AdaptiveOracleProgram (seedWidth domainWidth precision (inputWidth + 1) + inputWidth) outputWidth rounds) (hprecision : 0 < precision) (hlanguage : language ∈ PPoly) (hprogram : ∀ (oracle : BooleanOracle), oracle.Decides language → OracleProgramImplements precision (inputWidth + 1) setOfInput program oracle) : ∃ (circuitOracle : PolynomialCircuitOracle language) (fixed : Circuit Basis.andOr2 inputWidth outputWidth (program.inlineCircuitOracle circuitOracle).fst), (∀ (input : BitString inputWidth), OutputIsAccurate precision setOfInput input (fixed.eval input)) ∧ fixed.size = (program.inlineCircuitOracle circuitOracle).snd.size