Uniform polynomial-size circuits are in P — proof internals

theorem Complexity.circuitEvalLanguage_mem_P_internal : CircuitCode.circuitEvalLanguage ∈ P

Internal packaging of the verified serialized evaluator as a language in P.

theorem Complexity.UniformPPoly_subset_P_internal : UniformPPoly ⊆ P

Internal circuits-to-machines direction of logspace-uniform P/poly.