Tagged tuple interpretations: definitions

A TaggedFOInterpretation V W tags dim defines a target structure on the full universe Fin tags × (Fin dim → Fin A.card). Tags supply disjoint copies without using a built-in order. The target is presented on Fin (tags * A.card ^ dim) by Mathlib's finite product and tuple equivalences. Its size is exact.

Both the tag count and dimension are positive, so our convention card ≥ 2 is preserved. Target constants are tagged tuples of source constants. There are no domain restrictions or quotients. This module supplies the structure map; Interpretation.Pullback and Interpretation.Composition develop its logical transport and composition laws.

The tagged full-universe design follows Senellart and Gnatenko (2026), Sections 2.3 and 3.2, https://arxiv.org/abs/2609.18261. This implementation uses our finite vocabularies, de Bruijn formulas, and FinStruct presentation.

structure Complexity.DescriptiveComplexity.TaggedFOInterpretation (V W : Vocabulary) (tags dim : ℕ) : Type

An FO interpretation whose elements are tagged tuples of source elements.

• tags_pos : 0 < tags

  At least one disjoint copy of the tuple universe is present.

• dim_pos : 0 < dim

  Positive dimension preserves our minimum universe size.

• relFormula (i : Fin W.numRels) : (Fin (W.relArity i) → Fin tags) → Formula V (W.relArity i * dim)

  Each target relation is defined for each assignment of tags to its arguments.

• constTag : Fin W.numConsts → Fin tags

  The tag of each target constant.

• constCoord : Fin W.numConsts → Fin dim → Fin V.numConsts

  Each coordinate of a target constant is a source constant.

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.elementEquiv (card tags dim : ℕ) : Fin (tags * card ^ dim) ≃ Fin tags × (Fin dim → Fin card)

Decode the canonical finite presentation into a tag and a tuple.

Equations

• Complexity.DescriptiveComplexity.TaggedFOInterpretation.elementEquiv card tags dim = finProdFinEquiv.symm.trans ((Equiv.refl (Fin tags)).prodCongr finFunctionFinEquiv.symm)

def Complexity.DescriptiveComplexity.TaggedFOInterpretation.relationEnv {tags dim card arity : ℕ} (args : Fin arity → Fin (tags * card ^ dim)) : Env card (arity * dim)

Flatten a tuple of interpreted elements into the environment for a relation formula.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.DescriptiveComplexity.TaggedFOInterpretation.two_le_card {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : FinStruct V) : 2 ≤ tags * A.card ^ dim

The full interpreted universe still has at least two elements.

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.TaggedFOInterpretation.apply {V W : Vocabulary} {tags dim : ℕ} (I : TaggedFOInterpretation V W tags dim) (A : FinStruct V) : FinStruct W

Apply a tagged interpretation, using the full product universe. The abbreviation keeps the cardinality visible when transporting dependent variable environments.

Equations

• One or more equations did not get rendered due to their size.