First-order queries have nonuniform AC0 circuit families

At an encoded length choose the validated circuit. At every other positive length use a constant-false circuit. The empty input is also rejected. Monotone evaluation of natural polynomials transfers the universe-size bound to input length, and finite circuit witnesses assemble into the existing family model.

theorem Complexity.DescriptiveComplexity.sentence_circuits_internal {V : Vocabulary} (φ : Sentence V) (N : ℕ) [NeZero N] : ∃ (gates : ℕ) (c : Circuit Basis.unboundedAndOr N 1 gates), c.size ≤ Polynomial.eval N φ.validatedPolynomial ∧ c.depth ≤ Formula.size φ + 5 ∧ ∀ (input : BitString N), c.eval input 0 = queryFamily (fun (A : FinStruct V) => Sentence.Models A φ) N input

theorem Complexity.DescriptiveComplexity.sentence_mem_AC0_internal {V : Vocabulary} (φ : Sentence V) : (queryFamily fun (A : FinStruct V) => Sentence.Models A φ) ∈ AC0

theorem Complexity.DescriptiveComplexity.foDefinable_mem_AC0_internal {V : Vocabulary} {Q : BooleanQuery V} (hQ : FODefinable Q) : queryFamily Q ∈ AC0