First-order model checking by constant-depth Boolean circuits

Finite quantifier expansion produces the existing AC0Formula representation. For a fixed first-order formula, its tree size is exactly an explicit polynomial in universe size, and its depth is at most the source formula's size plus one. The same expansion handles every structure of the chosen size, including varying constant interpretations; the constants are supplied by one-hot input blocks. At positive input width, the expansion has an equivalent circuit with exactly the same size and depth at most the source formula's size plus two.

This formalizes the finite expansion step in Immerman, Theorem 5.22, Section 5.4 of Descriptive Complexity. DescriptiveComplexity.AC0 uses this expansion and encoding validation to prove the induced binary language has an AC0 family.

theorem Complexity.DescriptiveComplexity.StructureInput.compile_sat {V : Vocabulary} {N n : ℕ} (A : DecFinStruct V) (L : StructureInput V A.card N) (input : BitString N) (h : Represents A L input) (φ : Formula V n) (σ : Env A.card n) : AC0Formula.eval input (L.compile φ σ) = true ↔ Formula.Sat A.toFinStruct σ φ

The expansion computes first-order satisfaction on any represented structure.

theorem Complexity.DescriptiveComplexity.StructureInput.compile_size {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (φ : Formula V n) (σ : Env card n) : (L.compile φ σ).size = Polynomial.eval card φ.expansionPolynomial

Expansion has exact polynomial tree size, uniformly over assignments and layouts.

theorem Complexity.DescriptiveComplexity.StructureInput.compile_depth {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (φ : Formula V n) (σ : Env card n) : (L.compile φ σ).depth ≤ φ.size + 1

For a fixed source formula, expansion depth is independent of the universe size.

theorem Complexity.DescriptiveComplexity.StructureInput.exists_circuit {V : Vocabulary} {card N n : ℕ} [NeZero N] (L : StructureInput V card N) (φ : Formula V n) (σ : Env card n) : ∃ (gates : ℕ) (c : Circuit Basis.unboundedAndOr N 1 gates), c.size = Polynomial.eval card φ.expansionPolynomial ∧ c.depth ≤ φ.size + 2 ∧ ∀ (input : BitString N), c.eval input 0 = AC0Formula.eval input (L.compile φ σ)

At positive input width, one circuit realizes the expansion on every input. Its choice depends only on the formula, layout, and free-variable assignment.

theorem Complexity.DescriptiveComplexity.StructureInput.exists_circuit_sat {V : Vocabulary} {N n : ℕ} [NeZero N] (A : DecFinStruct V) (L : StructureInput V A.card N) (φ : Formula V n) (σ : Env A.card n) : ∃ (gates : ℕ) (c : Circuit Basis.unboundedAndOr N 1 gates), c.size = Polynomial.eval A.card φ.expansionPolynomial ∧ c.depth ≤ φ.size + 2 ∧ ∀ (input : BitString N), Represents A L input → (c.eval input 0 = true ↔ Formula.Sat A.toFinStruct σ φ)

The realized circuit decides satisfaction on every valid table input.

theorem Complexity.DescriptiveComplexity.Formula.table_expansion_sat {V : Vocabulary} {n : ℕ} (A : DecFinStruct V) (φ : Formula V n) (σ : Env A.card n) : AC0Formula.eval (tableInput A) ((tableLayout V A.card).compile φ σ) = true ↔ Sat A.toFinStruct σ φ

Every finite structure supplies a valid input to the fixed table-layout expansion.

theorem Complexity.DescriptiveComplexity.Sentence.table_expansion_models {V : Vocabulary} (A : DecFinStruct V) (φ : Sentence V) : AC0Formula.eval (tableInput A) ((tableLayout V A.card).compile φ (emptyEnv A.card)) = true ↔ Models A.toFinStruct φ

The sentence expansion decides the query on the structure's relation and constant tables.