Correctness of tagged formula pullback

The semantic induction uses coordinate evaluation and compatibility with tuple binders. Equality compares both the tag and every coordinate. Quantifiers range over the full tagged tuple universe, using elementEquiv to transfer witnesses.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.termCoords_eval {V W : Vocabulary} {tags dim n m : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : FinStruct V) (τ : Fin n → Fin tags) (κ : Fin n → Fin dim → Term V m) (σ : Env A.card m) (t : Term W n) : (elementEquiv A.card tags dim) (Term.eval (I.apply A) (coordEnv A τ κ σ) t) = (I.termTag τ t, fun (j : Fin dim) => Term.eval A σ (I.termCoords κ t j))

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.coordEnv_lift {V : Vocabulary} {tags dim n m : ℕ} (A : FinStruct V) (τ : Fin n → Fin tags) (κ : Fin n → Fin dim → Term V m) (σ : Env A.card m) (tag : Fin tags) (v : Env A.card dim) : coordEnv A (Fin.cons tag τ) (liftCoords κ) (envBlock σ v) = envCons ((elementEquiv A.card tags dim).symm (tag, v)) (coordEnv A τ κ σ)

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.relationEnv_evalTerms {V W : Vocabulary} {tags dim n m : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : FinStruct V) (τ : Fin n → Fin tags) (κ : Fin n → Fin dim → Term V m) (σ : Env A.card m) {arity : ℕ} (ts : Fin arity → Term W n) : (relationEnv fun (j : Fin arity) => Term.eval (I.apply A) (coordEnv A τ κ σ) (ts j)) = fun (k : Fin (arity * dim)) => Term.eval A σ (I.termCoords κ (ts (finProdFinEquiv.symm k).1) (finProdFinEquiv.symm k).2)

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.pullbackWith_sat {V W : Vocabulary} {tags dim n m : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : FinStruct V) (φ : Formula W n) (τ : Fin n → Fin tags) (κ : Fin n → Fin dim → Term V m) (σ : Env A.card m) : Formula.Sat A σ (I.pullbackWith φ τ κ) ↔ Formula.Sat (I.apply A) (coordEnv A τ κ σ) φ