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.expand (Λ : Language) (J : Type) [LinearOrder J] : FirstOrder.Language.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

The upper bound

The lower bound

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).