Exact cardinality of the local EM carrier (issue #11 unit 5)

The orbit code (LocalEMTupleOrbit.lean) deliberately forgets the J-locations of supports — so it cannot bound the carrier. The located term code restores them: LocatedTermCode Λ J := Σ k, (Fin k ↪o J) × Λ[[Fin k]].Term Empty — a compression arity, the increasing enumeration of the representative's support, and the compressed term. Since the embedding travels WITH the code, expansion is a total function (LocatedTermCode.expand), and locJExpand_compress makes the element-to-code map injective (locatedCode_injective).

• Upper bound (mk_carrier_le): compressed terms are countable (countable base language), Fin k ↪o J injects into Fin k → J, each finite power is at most max ℵ₀ #J, and the countable sigma stays there (CardinalBounds.mk_sigma_le_of_countable).
• Lower bound (mk_le_mk_carrier): for an INJECTIVE deep sequence the skeleton classes [c_j] are pairwise distinct — LocalEMEq on two constants would force the deep sequence to repeat at distinct ranks.
• Exact cardinality (mk_carrier): mk ctx.Carrier = max ℵ₀ (mk J) for infinite J, countable base language, injective deep sequence.

def FirstOrder.Language.LocatedTermCode (Λ : Language) (J : Type) [LinearOrder J] : Type

The located term code: compression arity, the support's increasing enumeration, and the compressed term. Unlike the orbit code, it remembers WHERE the support sits in J.

Equations

• Λ.LocatedTermCode J = ((k : ℕ) × (Fin k ↪o J) × (Λ.withConstants (Fin k)).Term Empty)

def FirstOrder.Language.LocatedTermCode.expand (Λ : Language) (J : Type) [LinearOrder J] : Λ.LocatedTermCode J → (Λ.withConstants J).Term Empty

Expansion of a located code — total, since the embedding travels with the code.

Equations

• FirstOrder.Language.LocatedTermCode.expand Λ J ⟨fst, (s, u)⟩ = Λ.locJExpand J s u

noncomputable def FirstOrder.Language.LocalEMContext.locatedCode {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (x : Carrier Λ J ctx) : Λ.LocatedTermCode J

The located code of a carrier element: enumerate its representative's support and compress.

Equations

• ctx.locatedCode x = ⟨(Λ.locJSupport J (Quotient.out x)).card, ((Λ.locJSupport J (Quotient.out x)).orderEmbOfFin ⋯, Λ.locJCompress J (Λ.locJSupport J (Quotient.out x)) (Quotient.out x) ⋯)⟩

theorem FirstOrder.Language.LocalEMContext.expand_locatedCode {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (x : Carrier Λ J ctx) : LocatedTermCode.expand Λ J (ctx.locatedCode x) = Quotient.out x

theorem FirstOrder.Language.LocalEMContext.locatedCode_injective {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) : Function.Injective ctx.locatedCode

The located code is injective: equal codes expand to equal representatives, hence equal classes.

The upper bound

theorem FirstOrder.Language.mk_locatedTermCode_le {Λ : Language} {J : Type} [LinearOrder J] [Countable ((l : ℕ) × Λ.Functions l)] : Cardinal.mk (Λ.LocatedTermCode J) ≤ max Cardinal.aleph0 (Cardinal.mk J)

The located-code type has size at most max ℵ₀ #J for a countable base language.

theorem FirstOrder.Language.LocalEMContext.mk_carrier_le {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) [Countable ((l : ℕ) × Λ.Functions l)] : Cardinal.mk (Carrier Λ J ctx) ≤ max Cardinal.aleph0 (Cardinal.mk J)

The upper bound: the carrier has size at most max ℵ₀ #J.

The lower bound

theorem FirstOrder.Language.LocalEMContext.mkClass_const_injective {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (hinj : Function.Injective ctx.a) : Function.Injective fun (j : J) => mkClass Λ J ctx (func (Sum.inr j) Fin.elim0)

Distinct skeleton constants have distinct classes for an injective deep sequence: LocalEMEq c_j c_{j'} would force a (d + r) = a (d + r') at distinct ranks.

theorem FirstOrder.Language.LocalEMContext.mk_le_mk_carrier {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (hinj : Function.Injective ctx.a) : Cardinal.mk J ≤ Cardinal.mk (Carrier Λ J ctx)

The lower bound: the skeleton injects into the carrier.

theorem FirstOrder.Language.LocalEMContext.mk_carrier_eq {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) [Countable ((l : ℕ) × Λ.Functions l)] [Infinite J] (hinj : Function.Injective ctx.a) : Cardinal.mk (Carrier Λ J ctx) = max Cardinal.aleph0 (Cardinal.mk J)

Exact carrier cardinality (issue #11 unit 5): for an infinite skeleton, a countable base language, and an injective deep sequence, mk ctx.Carrier = max ℵ₀ (mk J).