Skeleton compression: finite-support term codes

The generic compression layer of the countably-many-types project (issue #11 unit 3a), independent of the local EM quotient: a closed Λ[[J]]-term supported in a finite S : Finset J is coded by replacing each skeleton constant with its RANK in the increasing enumeration of S (locJCompress), forgetting the actual J-values while retaining the term shape and the equality/order pattern of the support. The inverse is expansion along any increasing embedding (locJExpand). The round trips:

• locJExpand_compress — expanding along S's own enumeration recovers the term;
• locJCompress_expand — compressing an expansion recovers the code;
• locJRename_expand — if e ∘ s = t pointwise then renaming along e carries the s-expansion to the t-expansion (the lemma the orbit theorem consumes);
• locJSupport_locJExpand — the support of an expansion is the image of the code's support.

The tuple-code type LocalEMTupleCode Λ n (Σ k, Fin n → Λ[[Fin k]].Term Empty) is COUNTABLE for a countable base language (countable_localEMTupleCode) — the quotient-tuple coding and the orbit theorem are unit 3b (LocalEMTupleOrbit.lean).

def FirstOrder.Language.locJCompress (Λ : Language) (J : Type) [LinearOrder J] (S : Finset J) (t : (Λ.withConstants J).Term Empty) : Λ.locJSupport J t ⊆ S → (Λ.withConstants (Fin S.card)).Term Empty

Skeleton compression: replace each skeleton constant of an S-supported closed term by its rank in the increasing enumeration of S.

Equations

• Λ.locJCompress J S (FirstOrder.Language.var e) x_2 = e.elim
• Λ.locJCompress J S (FirstOrder.Language.func (Sum.inl f') ts) h = FirstOrder.Language.func (Sum.inl f') fun (i : Fin l) => Λ.locJCompress J S (ts i) ⋯
• Λ.locJCompress J S (FirstOrder.Language.func (Sum.inr j) _ts) h = FirstOrder.Language.func (have this := Sum.inr ⟨FirstOrder.Language.deepRank J S j, ⋯⟩; this) Fin.elim0
• Λ.locJCompress J S (FirstOrder.Language.func (Sum.inr c) _ts) x_2 = PEmpty.elim c

def FirstOrder.Language.locJExpand (Λ : Language) (J : Type) [LinearOrder J] {k : ℕ} (s : Fin k ↪o J) {α : Type} (u : (Λ.withConstants (Fin k)).Term α) : (Λ.withConstants J).Term α

Skeleton expansion along an increasing embedding: interpret the Fin k constants by the embedded skeleton points.

Equations

• Λ.locJExpand J s u = (Λ.lhomWithConstantsMap ⇑s).onTerm u

theorem FirstOrder.Language.locJExpand_func_inl (Λ : Language) (J : Type) [LinearOrder J] {k : ℕ} (s : Fin k ↪o J) {α : Type} {l : ℕ} (f' : Λ.Functions l) (ts : Fin l → (Λ.withConstants (Fin k)).Term α) : Λ.locJExpand J s (func (Sum.inl f') ts) = func (Sum.inl f') fun (i : Fin l) => Λ.locJExpand J s (ts i)

theorem FirstOrder.Language.locJExpand_func_inr (Λ : Language) (J : Type) [LinearOrder J] {k : ℕ} (s : Fin k ↪o J) {α : Type} (i₀ : Fin k) (ts : Fin 0 → (Λ.withConstants (Fin k)).Term α) : Λ.locJExpand J s (func (Sum.inr i₀) ts) = func (Sum.inr (s i₀)) fun (i : Fin 0) => Λ.locJExpand J s (ts i)

theorem FirstOrder.Language.locJRename_func_inr (Λ : Language) (J : Type) [LinearOrder J] (e : J ≃o J) {α : Type} (j : J) (ts : Fin 0 → (Λ.withConstants J).Term α) : Λ.locJRename J e (func (Sum.inr j) ts) = func (Sum.inr (e j)) fun (i : Fin 0) => Λ.locJRename J e (ts i)

theorem FirstOrder.Language.locJSupport_locJExpand (Λ : Language) (J : Type) [LinearOrder J] {k : ℕ} (s : Fin k ↪o J) {α : Type} (u : (Λ.withConstants (Fin k)).Term α) : Λ.locJSupport J (Λ.locJExpand J s u) = Finset.image (⇑s) (Λ.locJSupport (Fin k) u)

The support of an expansion is the image of the code's support.

theorem FirstOrder.Language.locJExpand_compress (Λ : Language) (J : Type) [LinearOrder J] (S : Finset J) (t : (Λ.withConstants J).Term Empty) (h : Λ.locJSupport J t ⊆ S) : Λ.locJExpand J (S.orderEmbOfFin ⋯) (Λ.locJCompress J S t h) = t

Round trip 1: expanding along S's own increasing enumeration recovers the term.

theorem FirstOrder.Language.locJCompress_expand (Λ : Language) (J : Type) [LinearOrder J] (S : Finset J) (u : (Λ.withConstants (Fin S.card)).Term Empty) (h : Λ.locJSupport J (Λ.locJExpand J (S.orderEmbOfFin ⋯) u) ⊆ S) : Λ.locJCompress J S (Λ.locJExpand J (S.orderEmbOfFin ⋯) u) h = u

Round trip 2: compressing an expansion along S's enumeration recovers the code.

theorem FirstOrder.Language.locJRename_expand (Λ : Language) (J : Type) [LinearOrder J] (e : J ≃o J) {k : ℕ} (s t : Fin k ↪o J) (hst : ∀ (i : Fin k), e (s i) = t i) {α : Type} (u : (Λ.withConstants (Fin k)).Term α) : Λ.locJRename J e (Λ.locJExpand J s u) = Λ.locJExpand J t u

Round trip 3 (the orbit-theorem workhorse): if e carries the embedding s pointwise to t, then renaming along e carries the s-expansion to the t-expansion.

The countable tuple-code type

def FirstOrder.Language.LocalEMTupleCode (Λ : Language) (n : ℕ) : Type

The code of an n-tuple: a compression arity k together with n closed terms over the compressed skeleton Fin k.

Equations

• Λ.LocalEMTupleCode n = ((k : ℕ) × (Fin n → (Λ.withConstants (Fin k)).Term Empty))

theorem FirstOrder.Language.countable_sigma_functions_withFin (Λ : Language) (k : ℕ) [Countable ((l : ℕ) × Λ.Functions l)] : Countable ((l : ℕ) × (Λ.withConstants (Fin k)).Functions l)

Symbol countability passes to the constant expansion by a compressed skeleton.

theorem FirstOrder.Language.countable_localEMTupleCode (Λ : Language) (n : ℕ) [Countable ((l : ℕ) × Λ.Functions l)] : Countable (Λ.LocalEMTupleCode n)

Countability of the code type: for a countable base language, there are only countably many tuple codes at each arity.