Serialized evaluation circuits from polynomial circuit oracles -- internals

theorem Complexity.CircuitCode.EvaluationOracleCircuit.eval_queryCircuit_internal {codeWidth inputWidth : ℕ} [NeZero codeWidth] (code : BitString codeWidth) (input : BitString inputWidth) : ((queryCircuit codeWidth inputWidth).eval (packedInput code input)).toList = pair code.toList input.toList

theorem Complexity.CircuitCode.EvaluationOracleCircuit.eval_compile_internal (oracle : PolynomialCircuitOracle circuitEvalLanguage) {codeWidth inputWidth : ℕ} [NeZero codeWidth] (code : BitString codeWidth) (input : BitString inputWidth) : (compile oracle codeWidth inputWidth).snd.eval (packedInput code input) 0 = decide (evalFamilyCode code.toList input.toList = some true)

theorem Complexity.CircuitCode.EvaluationOracleCircuit.size_compile_internal (oracle : PolynomialCircuitOracle circuitEvalLanguage) (codeWidth inputWidth : ℕ) [NeZero codeWidth] : (compile oracle codeWidth inputWidth).snd.size = queryWidth codeWidth inputWidth + oracle.family.size (queryWidth codeWidth inputWidth)