Validated first-order circuits

Encoding validity has depth at most three and exact size card + 4 + numConsts * (1 + card * (1 + card)). Conjoining this test with the sentence expansion gives exact query-language semantics on every input of the chosen encoded length, including malformed strings.

theorem Complexity.DescriptiveComplexity.encodingValidityFormula_correct (V : Vocabulary) (card : ℕ) (input : BitString (encodingLength V card)) : AC0Formula.eval input (encodingValidityFormula V card) = true ↔ ∃ (A : DecFinStruct V), encodeStruct A = List.ofFn input

The validator accepts exactly the encodings at the chosen input length.

theorem Complexity.DescriptiveComplexity.encodingValidityFormula_size (V : Vocabulary) (card : ℕ) : (encodingValidityFormula V card).size = Polynomial.eval card (encodingValidityPolynomial V)

Encoding validation has an exact size polynomial of degree at most two.

theorem Complexity.DescriptiveComplexity.encodingValidityFormula_depth (V : Vocabulary) (card : ℕ) : (encodingValidityFormula V card).depth ≤ 3

Encoding validation has depth at most three, independently of universe size.

theorem Complexity.DescriptiveComplexity.Sentence.validatedExpansion_correct {V : Vocabulary} (φ : Sentence V) (card : ℕ) (input : BitString (encodingLength V card)) : AC0Formula.eval input (φ.validatedExpansion card) = true ↔ List.ofFn input ∈ queryLanguage fun (A : FinStruct V) => Models A φ

Validated expansion recognizes the exact induced language at this encoded length.

theorem Complexity.DescriptiveComplexity.Sentence.validatedExpansion_size {V : Vocabulary} (φ : Sentence V) (card : ℕ) : (φ.validatedExpansion card).size = Polynomial.eval card φ.validatedPolynomial

The complete validated expansion has exact polynomial size.

theorem Complexity.DescriptiveComplexity.Sentence.validatedExpansion_depth {V : Vocabulary} (φ : Sentence V) (card : ℕ) : (φ.validatedExpansion card).depth ≤ Formula.size φ + 4

Validation adds only a constant number of depth layers to sentence expansion.

theorem Complexity.DescriptiveComplexity.Sentence.exists_validated_circuit {V : Vocabulary} (φ : Sentence V) (card : ℕ) : ∃ (gates : ℕ) (c : Circuit Basis.unboundedAndOr (encodingLength V card) 1 gates), c.size = Polynomial.eval card φ.validatedPolynomial ∧ c.depth ≤ Formula.size φ + 5 ∧ ∀ (input : BitString (encodingLength V card)), c.eval input 0 = true ↔ List.ofFn input ∈ queryLanguage fun (A : FinStruct V) => Models A φ

Actual circuit realizations decide the query on every input of the encoded length.