Correctness of canonical numerical expansion

The two blocks of the extended vocabulary respectively recover the input relations and the designated numerical predicates. Forgetting the second block recovers the original structure, so the existing interpretation transport theorem also proves correctness of embedding input formulas.

theorem Complexity.DescriptiveComplexity.forgetNumerical_apply_internal {V : Vocabulary} (A : FinStruct V) (predicates : List NumericalPredicate) : (FOInterpretation.forgetNumerical V predicates).apply (A.withNumerical predicates) = A

theorem Complexity.DescriptiveComplexity.withNumerical_sat_internal {V : Vocabulary} {n : ℕ} (A : FinStruct V) (φ : Formula V n) (predicates : List NumericalPredicate) (σ : Env A.card n) : Formula.Sat (A.withNumerical predicates) σ (φ.withNumerical predicates) ↔ Formula.Sat A σ φ

theorem Complexity.DescriptiveComplexity.numerical_sat_internal {V : Vocabulary} {n : ℕ} (A : FinStruct V) (predicates : List NumericalPredicate) (r : Fin predicates.length) (args : Fin (predicates.get r).arity → Term (V.withNumerical predicates) n) (σ : Env A.card n) : Formula.Sat (A.withNumerical predicates) σ (Formula.numerical predicates r args) ↔ (predicates.get r).Holds fun (i : Fin (predicates.get r).arity) => ↑(Term.eval (A.withNumerical predicates) σ (args i))

theorem Complexity.DescriptiveComplexity.withNumerical_toFinStruct_internal {V : Vocabulary} (A : DecFinStruct V) (predicates : List NumericalPredicate) : (A.withNumerical predicates).toFinStruct = A.toFinStruct.withNumerical predicates