Correctness and bounds for finite quantifier expansion

Atomic selectors read the represented structure. The formula induction expands finite quantification and gives exact polynomial tree size and constant depth.

theorem Complexity.DescriptiveComplexity.StructureInput.termTest_true {V : Vocabulary} {N n : ℕ} (A : DecFinStruct V) (L : StructureInput V A.card N) (input : BitString N) (h : Represents A L input) (σ : Env A.card n) (t : Term V n) (a : Fin A.card) : AC0Formula.eval input (L.termTest σ t a) = true ↔ Term.eval A.toFinStruct σ t = a

theorem Complexity.DescriptiveComplexity.StructureInput.relationTest_true {V : Vocabulary} {N n : ℕ} (A : DecFinStruct V) (L : StructureInput V A.card N) (input : BitString N) (h : Represents A L input) (σ : Env A.card n) (i : Fin V.numRels) (ts : Fin (V.relArity i) → Term V n) : AC0Formula.eval input (L.relationTest σ i ts) = true ↔ (A.rel i fun (j : Fin (V.relArity i)) => Term.eval A.toFinStruct σ (ts j)) = true

theorem Complexity.DescriptiveComplexity.StructureInput.equalityTest_true {V : Vocabulary} {N n : ℕ} (A : DecFinStruct V) (L : StructureInput V A.card N) (input : BitString N) (h : Represents A L input) (σ : Env A.card n) (t₁ t₂ : Term V n) : AC0Formula.eval input (L.equalityTest σ t₁ t₂) = true ↔ Term.eval A.toFinStruct σ t₁ = Term.eval A.toFinStruct σ t₂

theorem Complexity.DescriptiveComplexity.StructureInput.compile_sat_internal {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 σ φ

theorem Complexity.DescriptiveComplexity.StructureInput.termTest_size {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (σ : Env card n) (t : Term V n) (a : Fin card) : (L.termTest σ t a).size = 1

theorem Complexity.DescriptiveComplexity.StructureInput.termTest_depth {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (σ : Env card n) (t : Term V n) (a : Fin card) : (L.termTest σ t a).depth = 0

theorem Complexity.DescriptiveComplexity.StructureInput.relationTest_size {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (σ : Env card n) (i : Fin V.numRels) (ts : Fin (V.relArity i) → Term V n) : (L.relationTest σ i ts).size = 1 + card ^ V.relArity i * (V.relArity i + 2)

theorem Complexity.DescriptiveComplexity.StructureInput.equalityTest_size {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (σ : Env card n) (t₁ t₂ : Term V n) : (L.equalityTest σ t₁ t₂).size = 1 + card * 3

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

theorem Complexity.DescriptiveComplexity.StructureInput.relationTest_depth_le {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (σ : Env card n) (i : Fin V.numRels) (ts : Fin (V.relArity i) → Term V n) : (L.relationTest σ i ts).depth ≤ 2

theorem Complexity.DescriptiveComplexity.StructureInput.equalityTest_depth_le {V : Vocabulary} {card N n : ℕ} (L : StructureInput V card N) (σ : Env card n) (t₁ t₂ : Term V n) : (L.equalityTest σ t₁ t₂).depth ≤ 2

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