Shared generic support for the EM term-model constructions

Language-independent lemmas consumed by BOTH the original skolemColim-based EM term model (EMTermModel.lean) and the countable local stack (LocalEMFamily.lean / LocalEMContext.lean) — extracted here (2026-07-02) so the local stack does not have to import EMTermModel.lean:

• two Mathlib-gap Term lemmas: Term.varFinset_relabel and Term.realize_eq_of_eq_on_varFinset;
• the ordered-support rank machinery deepRank (the 0-indexed position of an element in a finite J-support, in increasing order) with its inverse/monotonicity lemmas against Finset.orderEmbOfFin.

theorem FirstOrder.Language.Term.varFinset_relabel {L' : Language} {α β : Type} [DecidableEq α] [DecidableEq β] (g : α → β) (t : L'.Term α) : (relabel g t).varFinset = Finset.image g t.varFinset

The variables of a relabeled term are the image of the original variables (a Mathlib gap).

theorem FirstOrder.Language.Term.realize_eq_of_eq_on_varFinset {L' : Language} {M' : Type} [L'.Structure M'] {α : Type} [DecidableEq α] {v w : α → M'} (t : L'.Term α) : (∀ x ∈ t.varFinset, v x = w x) → realize v t = realize w t

A term's realization depends only on the assignment of the variables that actually appear (a Mathlib gap).

Ordered support (ranks)

def FirstOrder.Language.deepRank (J : Type) [LinearOrder J] (S : Finset J) (j : J) : ℕ

The rank of j in a finite support S: the number of support elements below it, i.e. its 0-indexed position in the increasing J-order. So a support {j₀ < j₁ < …} has ranks 0, 1, … and the deep interpretation sends it to a_d, a_{d+1}, … (a strictly-increasing deep tuple).

Equations

• FirstOrder.Language.deepRank J S j = {x ∈ S | x < j}.card

theorem FirstOrder.Language.deepRank_lt_of_lt (J : Type) [LinearOrder J] {S : Finset J} {j j' : J} (hj : j ∈ S) (hjj' : j < j') : deepRank J S j < deepRank J S j'

On the support, ranks strictly increase with J-order: the deep tuple is strictly increasing, hence injective on the support.

theorem FirstOrder.Language.deepRank_orderEmbOfFin (J : Type) [LinearOrder J] (S : Finset J) {k : ℕ} (h : S.card = k) (i : Fin k) : deepRank J S ((S.orderEmbOfFin h) i) = ↑i

The rank of the i-th support element (in increasing order) is i: the enumeration orderEmbOfFin and the rank are mutually inverse. The elements of S strictly below the i-th are exactly the first i.

theorem FirstOrder.Language.deepRank_lt_card (J : Type) [LinearOrder J] {S : Finset J} {j : J} (hj : j ∈ S) : deepRank J S j < S.card

The rank of a support element is below the cardinality: a valid Fin S.card position.

theorem FirstOrder.Language.orderEmbOfFin_deepRank (J : Type) [LinearOrder J] (S : Finset J) {k : ℕ} (h : S.card = k) {j : J} (hj : j ∈ S) (hlt : deepRank J S j < k) : (S.orderEmbOfFin h) ⟨deepRank J S j, hlt⟩ = j

The enumeration recovers a support element from its rank: orderEmbOfFin at position deepRank S j is j, for j ∈ S.