From 6975e34b3325025e88e19d9289cd3aedb6ba47b0 Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Thu, 23 Jul 2026 18:15:00 +0800
Subject: [PATCH 01/11] feat(Data/Set/Card): characterize finite lower bounds
 on encard

---
 Mathlib/Data/Set/Card.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean
index 52b8f13cd2f277..e1c1d155b136e4 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -479,6 +479,22 @@ theorem exists_subset_encard_eq {k : ℕ∞} (hk : k ≤ s.encard) : ∃ t, t 
     exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩
   | top => rw [top_le_iff] at hk; exact ⟨s, Subset.rfl, hk⟩
 
+/-- An injection from `Fin n` into a set is equivalent to a lower bound of `n` on its extended
+cardinality. -/
+theorem le_encard_iff_exists_injection_fin (s : Set α) (n : ℕ) :
+    (n : ℕ∞) ≤ s.encard ↔ ∃ f : Fin n → α, (∀ i, f i ∈ s) ∧ Function.Injective f := by
+  constructor
+  · intro h
+    obtain ⟨t, hts, hte⟩ := exists_subset_encard_eq h
+    letI := (finite_of_encard_eq_coe hte).fintype
+    let e := Fintype.equivFinOfCardEq <| ENat.natCast_inj.mp <| (coe_fintypeCard t).trans hte
+    exact ⟨Subtype.val ∘ e.symm, fun i ↦ hts (e.symm i).2,
+      (Equiv.injective_comp e.symm Subtype.val).mpr Subtype.val_injective⟩
+  · rintro ⟨f, hf, hfi⟩
+    simpa only [ENat.card_eq_coe_fintype_card, Fintype.card_fin,
+      ENat.card_coe_set_eq] using ENat.card_le_card_of_injective
+        (f := fun i : Fin n ↦ ⟨f i, hf i⟩) (fun _ _ hi ↦ hfi (Subtype.ext_iff.mp hi))
+
 theorem exists_superset_subset_encard_eq {k : ℕ∞}
     (hst : s ⊆ t) (hsk : s.encard ≤ k) (hkt : k ≤ t.encard) :
     ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k := by

From 056ce0d91adf50f2cef397f858dc5f8ca01703dd Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Thu, 23 Jul 2026 18:38:20 +0800
Subject: [PATCH 02/11] feat(ModelTheory): add counting formulas

---
 Mathlib/ModelTheory/Semantics.lean | 82 +++++++++++++++++++++++++++++-
 Mathlib/ModelTheory/Syntax.lean    | 28 ++++++++++
 2 files changed, 109 insertions(+), 1 deletion(-)

diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean
index 18e86ea15e52f5..b2d3a2305d2b44 100644
--- a/Mathlib/ModelTheory/Semantics.lean
+++ b/Mathlib/ModelTheory/Semantics.lean
@@ -6,8 +6,9 @@ Authors: Aaron Anderson, Jesse Michael Han, Floris van Doorn
 module
 
 public import Mathlib.Data.Finset.Basic
-public import Mathlib.ModelTheory.Syntax
 public import Mathlib.Data.List.ProdSigma
+public import Mathlib.Data.Set.Card
+public import Mathlib.ModelTheory.Syntax
 
 /-!
 # Basics on First-Order Semantics
@@ -33,6 +34,9 @@ in a style inspired by the [Flypitch project](https://flypitch.github.io/).
 - Several results in this file show that syntactic constructions such as `relabel`, `castLE`,
   `liftAt`, `subst`, and the actions of language maps commute with realization of terms, formulas,
   sentences, and theories.
+- `FirstOrder.Language.Formula.realize_iExsAtLeast`, `realize_iExsAtMost`, and
+  `realize_iExsExactly` characterize counting formulas using the extended cardinality of their
+  realization sets.
 
 ## Implementation Notes
 
@@ -942,6 +946,82 @@ end BoundedFormula
 
 namespace Formula
 
+/-- Realization of `iExsAtLeast` is equivalent to the existence of an injective family of `n`
+pairwise distinct realizing assignments to the `β`-variables. -/
+theorem realize_iExsAtLeast_iff_exists_injective [Finite β]
+    (φ : L.Formula (α ⊕ β)) (v : α → M) (n : ℕ) :
+    (φ.iExsAtLeast β n).Realize v ↔
+      ∃ f : Fin n → (β → M), (∀ i, φ.Realize (Sum.elim v (f i))) ∧ Function.Injective f := by
+  simp only [iExsAtLeast, ne_eq, realize_iExs, realize_inf, realize_iInf, realize_relabel,
+    realize_not, realize_equal, Term.realize_var, Sum.elim_inr, not_forall, Subtype.forall,
+    Prod.forall]
+  refine (Equiv.curry (Fin n) β M).exists_congr fun u ↦ and_congr ?_ ?_
+  · refine forall_congr' fun i ↦ iff_of_eq <| congrArg φ.Realize ?_
+    funext x
+    cases x <;> rfl
+  · rw [Function.injective_iff_pairwise_ne]
+    simp [Pairwise, funext_iff, Function.onFun]
+
+/-- The formula `iExsAtLeast β n φ` is realized exactly when the realization set of `φ` has
+extended cardinality at least `n`. -/
+@[simp]
+theorem realize_iExsAtLeast [Finite β] (φ : L.Formula (α ⊕ β)) (v : α → M) (n : ℕ) :
+    (φ.iExsAtLeast β n).Realize v ↔
+      (n : ℕ∞) ≤ {x : β → M | φ.Realize (Sum.elim v x)}.encard := by
+  simp only [realize_iExsAtLeast_iff_exists_injective, Set.le_encard_iff_exists_injection_fin,
+    Set.mem_ofPred_eq]
+
+/-- The formula `iExsAtMost β n φ` is realized exactly when the realization set of `φ` has
+extended cardinality at most `n`. -/
+@[simp]
+theorem realize_iExsAtMost [Finite β] (φ : L.Formula (α ⊕ β)) (v : α → M) (n : ℕ) :
+    (φ.iExsAtMost β n).Realize v ↔
+      {x : β → M | φ.Realize (Sum.elim v x)}.encard ≤ n := by
+  simpa [iExsAtMost] using ENat.lt_natCast_add_one_iff
+
+/-- The formula `iExsExactly β n φ` is realized exactly when the realization set of `φ` has
+extended cardinality `n`. -/
+@[simp]
+theorem realize_iExsExactly [Finite β] (φ : L.Formula (α ⊕ β)) (v : α → M) (n : ℕ) :
+    (φ.iExsExactly β n).Realize v ↔
+      {x : β → M | φ.Realize (Sum.elim v x)}.encard = n := by
+  simpa [iExsExactly] using Iff.symm ge_antisymm_iff
+
+/-- Exact cardinality zero means there is no realizing assignment to the `β`-variables. -/
+theorem realize_iExsExactly_zero [Finite β] (φ : L.Formula (α ⊕ β)) (v : α → M) :
+    (φ.iExsExactly β 0).Realize v ↔ ¬∃ x : β → M, φ.Realize (Sum.elim v x) := by
+  simp only [realize_iExsExactly, Nat.cast_zero, Set.encard_eq_zero, not_exists]
+  exact Set.eq_empty_iff_forall_notMem
+
+/-- Exact cardinality one is semantically equivalent to unique existence. -/
+theorem realize_iExsExactly_one_iff_iExsUnique [Finite β]
+    (φ : L.Formula (α ⊕ β)) (v : α → M) :
+    (φ.iExsExactly β 1).Realize v ↔ (φ.iExsUnique β).Realize v := by
+  rw [realize_iExsExactly, Nat.cast_one, realize_iExsUnique, Set.encard_eq_one]
+  constructor
+  · rintro ⟨x, hx⟩
+    have hmem := Set.ext_iff.mp hx
+    exact ⟨x, (hmem x).2 rfl, fun y hy ↦ (hmem y).1 hy⟩
+  · rintro ⟨x, hx, hunique⟩
+    refine ⟨x, Set.ext fun y ↦ ?_⟩
+    simp only [Set.mem_ofPred_eq, Set.mem_singleton_iff]
+    exact ⟨hunique y, fun hy ↦ hy ▸ hx⟩
+
+/-- Having at most `n` realizations is the negation of having at least `n + 1` realizations. -/
+theorem realize_iExsAtMost_iff_not_iExsAtLeast_succ [Finite β]
+    (φ : L.Formula (α ⊕ β)) (v : α → M) (n : ℕ) :
+    (φ.iExsAtMost β n).Realize v ↔ ¬(φ.iExsAtLeast β (n + 1)).Realize v := by
+  simpa using Iff.symm ENat.lt_natCast_add_one_iff
+
+/-- Having at most `n` realizations rules out any injective family of `n + 1` realizations. -/
+theorem realize_iExsAtMost_iff_not_exists_injection [Finite β]
+    (φ : L.Formula (α ⊕ β)) (v : α → M) (n : ℕ) :
+    (φ.iExsAtMost β n).Realize v ↔
+      ¬∃ f : Fin (n + 1) → (β → M),
+        (∀ i, φ.Realize (Sum.elim v (f i))) ∧ Function.Injective f := by
+  simpa only [realize_iExsAtMost_iff_not_iExsAtLeast_succ] using
+    not_congr (realize_iExsAtLeast_iff_exists_injective φ v (n + 1))
+
 @[simp]
 theorem realize_exClosure [DecidableEq α] (φ : L.Formula α) :
     φ.exClosure.Realize M ↔
diff --git a/Mathlib/ModelTheory/Syntax.lean b/Mathlib/ModelTheory/Syntax.lean
index 91e8e540b6891f..272a8d4d0455d1 100644
--- a/Mathlib/ModelTheory/Syntax.lean
+++ b/Mathlib/ModelTheory/Syntax.lean
@@ -22,6 +22,8 @@ This file defines first-order terms, formulas, sentences, and theories in a styl
   variables indexed by `α`.
 - A `FirstOrder.Language.Formula` is defined so that `L.Formula α` is the type of `L`-formulas with
   free variables indexed by `α`.
+- `FirstOrder.Language.Formula.iExsAtLeast`, `iExsAtMost`, and `iExsExactly` express finite
+  cardinality bounds on the set of realizations of a formula.
 - A `FirstOrder.Language.Sentence` is a formula with no free variables.
 - A `FirstOrder.Language.Theory` is a set of sentences.
 - The variables of terms and formulas can be relabelled with `FirstOrder.Language.Term.relabel`,
@@ -809,6 +811,32 @@ to equivalence of formulas. -/
 noncomputable def iInf [Finite α] (f : α → L.Formula β) : L.Formula β :=
   BoundedFormula.iInf f
 
+variable (β) in
+/-- Asserts that `φ` has at least `n` pairwise distinct realizations as assignments to the
+`β`-variables. -/
+noncomputable def iExsAtLeast [Finite β] (n : ℕ) (φ : L.Formula (α ⊕ β)) : L.Formula α :=
+  let realizeAt (i : Fin n) : L.Formula (α ⊕ (Fin n × β)) :=
+    φ.relabel (Sum.map id fun b ↦ (i, b))
+  let tupleNe (i j : Fin n) : L.Formula (α ⊕ (Fin n × β)) :=
+    (iInf fun b : β ↦
+      (Term.var (Sum.inr (i, b))).equal (Term.var (Sum.inr (j, b)))).not
+  let NePair := {ij : Fin n × Fin n // ij.1 ≠ ij.2}
+  let witnessesRealize : L.Formula (α ⊕ (Fin n × β)) :=
+    iInf fun i : Fin n ↦ realizeAt i
+  let witnessesDistinct : L.Formula (α ⊕ (Fin n × β)) :=
+    iInf fun ij : NePair ↦ tupleNe ij.1.1 ij.1.2
+  (witnessesRealize ⊓ witnessesDistinct).iExs (Fin n × β)
+
+variable (β) in
+/-- Asserts that `φ` has at most `n` realizations as assignments to the `β`-variables. -/
+noncomputable def iExsAtMost [Finite β] (n : ℕ) (φ : L.Formula (α ⊕ β)) : L.Formula α :=
+  (φ.iExsAtLeast β (n + 1)).not
+
+variable (β) in
+/-- Asserts that `φ` has exactly `n` realizations as assignments to the `β`-variables. -/
+noncomputable def iExsExactly [Finite β] (n : ℕ) (φ : L.Formula (α ⊕ β)) : L.Formula α :=
+  φ.iExsAtLeast β n ⊓ φ.iExsAtMost β n
+
 /-- A bijection sending formulas to sentences with constants. -/
 def equivSentence : L.Formula α ≃ L[[α]].Sentence :=
   (BoundedFormula.constantsVarsEquiv.trans (BoundedFormula.relabelEquiv (Equiv.sumEmpty _ _))).symm

From 1c479dcc21114fef2afc3c7f2a10c436cf63c7de Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Thu, 23 Jul 2026 19:02:48 +0800
Subject: [PATCH 03/11] feat(ModelTheory/ElementaryMaps): preserve
 definable-set cardinality

---
 Mathlib/ModelTheory/ElementaryMaps.lean | 45 +++++++++++++++++++++++++
 1 file changed, 45 insertions(+)

diff --git a/Mathlib/ModelTheory/ElementaryMaps.lean b/Mathlib/ModelTheory/ElementaryMaps.lean
index d84e4419ec067f..3a82db25bcab1d 100644
--- a/Mathlib/ModelTheory/ElementaryMaps.lean
+++ b/Mathlib/ModelTheory/ElementaryMaps.lean
@@ -22,6 +22,12 @@ public import Mathlib.ModelTheory.Substructures
 
 ## Main Results
 
+- `FirstOrder.Language.ElementaryEmbedding.mk_realizations_le` shows that definable-set
+  cardinality cannot decrease under an elementary embedding.
+- `FirstOrder.Language.ElementaryEmbedding.encard_realizations_eq_coe_iff` shows that elementary
+  embeddings preserve exact finite definable-set cardinality.
+- `FirstOrder.Language.ElementaryEmbedding.infinite_realizations_iff` shows that elementary
+  embeddings preserve and reflect infinitude of definable sets.
 - The Tarski-Vaught Test for embeddings: `FirstOrder.Language.Embedding.isElementary_of_exists`
   gives a simple criterion for an embedding to be elementary.
 -/
@@ -30,6 +36,7 @@ public import Mathlib.ModelTheory.Substructures
 
 
 open FirstOrder
+open scoped Cardinal
 
 namespace FirstOrder
 
@@ -110,6 +117,44 @@ theorem injective (φ : M ↪ₑ[L] N) : Function.Injective φ := by
 instance embeddingLike : EmbeddingLike (M ↪ₑ[L] N) M N :=
   { show FunLike (M ↪ₑ[L] N) M N from inferInstance with injective' := injective }
 
+section
+
+universe u u' v v'
+
+variable {M : Type u} {N : Type u'} {α : Type v} {β : Type v'}
+variable [L.Structure M] [L.Structure N]
+
+/-- The embedding of realization subtypes induced by an elementary embedding. -/
+def realizationsEmbedding (e : M ↪ₑ[L] N) (φ : L.Formula (β ⊕ α)) (b : β → M) :
+    {x : α → M | φ.Realize (Sum.elim b x)} ↪
+      {x : α → N | φ.Realize (Sum.elim (e ∘ b) x)} where
+  toFun x := ⟨e ∘ x, show φ.Realize _ by
+    simpa only [← Sum.comp_elim] using (e.map_formula φ (Sum.elim b x)).mpr x.2⟩
+  inj' x y h := Subtype.ext <| e.injective.comp_left <| congrArg Subtype.val h
+
+/-- Cardinality of a definable set cannot decrease under an elementary embedding. -/
+theorem mk_realizations_le (e : M ↪ₑ[L] N) (φ : L.Formula (β ⊕ α)) (b : β → M) :
+    Cardinal.lift.{max u' v} (#({x : α → M | φ.Realize (Sum.elim b x)})) ≤
+      Cardinal.lift.{max u v} (#({x : α → N | φ.Realize (Sum.elim (e ∘ b) x)})) :=
+  Cardinal.lift_mk_le_lift_mk_of_injective (realizationsEmbedding e φ b).injective
+
+/-- An elementary embedding preserves and reflects exact finite cardinality of a definable set. -/
+theorem encard_realizations_eq_coe_iff [Finite α] (e : M ↪ₑ[L] N)
+    (φ : L.Formula (β ⊕ α)) (b : β → M) (n : ℕ) :
+    {x : α → N | φ.Realize (Sum.elim (e ∘ b) x)}.encard = n ↔
+      {x : α → M | φ.Realize (Sum.elim b x)}.encard = n := by
+  simp only [← Formula.realize_iExsExactly, map_formula]
+
+/-- The infititude of a definable set is preserved under an elementary embedding. -/
+theorem infinite_realizations_iff [Finite α] (e : M ↪ₑ[L] N)
+    (φ : L.Formula (β ⊕ α)) (b : β → M) :
+    Set.Infinite {x : α → N | φ.Realize (Sum.elim (e ∘ b) x)} ↔
+      Set.Infinite {x : α → M | φ.Realize (Sum.elim b x)} := by
+  simp [Set.encard_eq_top_iff.symm.trans ENat.eq_top_iff_forall_ge,
+    ← Formula.realize_iExsAtLeast]
+
+end
+
 @[simp]
 theorem map_fun (φ : M ↪ₑ[L] N) {n : ℕ} (f : L.Functions n) (x : Fin n → M) :
     φ (funMap f x) = funMap f (φ ∘ x) := by

From 082166b43a7ce8ff70c6f0ca0dbbef0aeda69121 Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Thu, 23 Jul 2026 19:06:10 +0800
Subject: [PATCH 04/11] fix typo

---
 Mathlib/ModelTheory/ElementaryMaps.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/ModelTheory/ElementaryMaps.lean b/Mathlib/ModelTheory/ElementaryMaps.lean
index 3a82db25bcab1d..45b59ecdc828b8 100644
--- a/Mathlib/ModelTheory/ElementaryMaps.lean
+++ b/Mathlib/ModelTheory/ElementaryMaps.lean
@@ -145,7 +145,7 @@ theorem encard_realizations_eq_coe_iff [Finite α] (e : M ↪ₑ[L] N)
       {x : α → M | φ.Realize (Sum.elim b x)}.encard = n := by
   simp only [← Formula.realize_iExsExactly, map_formula]
 
-/-- The infititude of a definable set is preserved under an elementary embedding. -/
+/-- The infinitude of a definable set is preserved under an elementary embedding. -/
 theorem infinite_realizations_iff [Finite α] (e : M ↪ₑ[L] N)
     (φ : L.Formula (β ⊕ α)) (b : β → M) :
     Set.Infinite {x : α → N | φ.Realize (Sum.elim (e ∘ b) x)} ↔

From 6b208109dc50a429c1ae804f2af9d67df7627208 Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Mon, 27 Jul 2026 13:51:46 +0800
Subject: [PATCH 05/11] feat(SetTheory/Cardinal): add cardinality bounds for
 direct limits

---
 Mathlib.lean                                |  1 +
 Mathlib/Order/DirectedInverseSystem.lean    | 11 +++
 Mathlib/SetTheory/Cardinal/DirectLimit.lean | 97 +++++++++++++++++++++
 3 files changed, 109 insertions(+)
 create mode 100644 Mathlib/SetTheory/Cardinal/DirectLimit.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 29db19960dc526..2926f132d98b81 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -7182,6 +7182,7 @@ public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
 public import Mathlib.SetTheory.Cardinal.Continuum
 public import Mathlib.SetTheory.Cardinal.CountableCover
 public import Mathlib.SetTheory.Cardinal.Defs
+public import Mathlib.SetTheory.Cardinal.DirectLimit
 public import Mathlib.SetTheory.Cardinal.Divisibility
 public import Mathlib.SetTheory.Cardinal.ENNReal
 public import Mathlib.SetTheory.Cardinal.ENat
diff --git a/Mathlib/Order/DirectedInverseSystem.lean b/Mathlib/Order/DirectedInverseSystem.lean
index 468e2e921a06d6..d70ce590de1c6e 100644
--- a/Mathlib/Order/DirectedInverseSystem.lean
+++ b/Mathlib/Order/DirectedInverseSystem.lean
@@ -185,6 +185,17 @@ theorem lift_injective (h : ∀ i, Function.Injective (ih i)) :
 
 end lift
 
+/-- If `m` is an upper bound for the index type, then the direct limit is equivalent to the
+component at `m`. -/
+def equivOfForallLE (m : ι) (hm : ∀ i, i ≤ m) : DirectLimit F f ≃ F m where
+  toFun := DirectLimit.lift f (fun i x ↦ f i m (hm i) x) (by simp [map_map'])
+  invFun := fun x ↦ ⟦⟨m,x⟩⟧
+  left_inv := by
+    intro z
+    induction z using DirectLimit.induction with
+    | _ i x => simp only [lift_def, mk_apply]
+  right_inv := fun _ ↦ by simp only [lift_def, map_self']
+
 section map
 
 variable (ih : ∀ i, F₁ i → F₂ i) (compat : ∀ i j h x, f₂ i j h (ih i x) = ih j (f₁ i j h x))
diff --git a/Mathlib/SetTheory/Cardinal/DirectLimit.lean b/Mathlib/SetTheory/Cardinal/DirectLimit.lean
new file mode 100644
index 00000000000000..030c453fe309cd
--- /dev/null
+++ b/Mathlib/SetTheory/Cardinal/DirectLimit.lean
@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2026 Zikang Yu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zikang Yu
+-/
+module
+
+public import Mathlib.Data.Fintype.Order
+public import Mathlib.Order.DirectedInverseSystem
+public import Mathlib.SetTheory.Cardinal.Arithmetic
+
+/-!
+# Cardinality of direct limits
+
+This file gives upper and lower bounds for the cardinality of a direct limit of types.
+
+## Main statements
+
+* `DirectLimit.mk_le_sum`: the cardinality of a direct limit is at most the sum of the
+  cardinalities of its components.
+* `DirectLimit.mk_le_of_aleph0_le`: an infinite common bound for the index type and the
+  components is also a bound for the direct limit.
+* `DirectLimit.iSup_lift_mk_le_mk`: when the canonical maps are injective, the supremum of the
+  component cardinalities is at most the cardinality of the direct limit.
+* `DirectLimit.mk_eq_iSup_lift_mk`: when that supremum is greater than the cardinality of the
+  index type and the canonical maps are injective, it equals the cardinality of the direct limit.
+* `DirectLimit.mk_eq_of_forall_lift_mk_eq`: when all components have the same cardinality, under
+  the corresponding bound and injectivity assumptions, so does the direct limit.
+-/
+
+@[expose] public section
+
+open Cardinal Function
+
+universe u v w
+
+namespace DirectLimit
+
+variable {ι : Type u} [Preorder ι] {F : ι → Type v}
+variable {T : ∀ ⦃i j : ι⦄, i ≤ j → Sort w} (f : ∀ i j (h : i ≤ j), T h)
+variable [∀ ⦃i j⦄ (h : i ≤ j), FunLike (T h) (F i) (F j)]
+variable [DirectedSystem F (f · · ·)] [IsDirectedOrder ι]
+
+/-- The cardinality of a direct limit is at most the sum of the cardinalities of its
+components. -/
+theorem mk_le_sum : #(DirectLimit F (f · · ·)) ≤ Cardinal.sum fun i ↦ #(F i) :=
+  mk_quotient_le.trans_eq (mk_sigma F)
+
+/-- An infinite cardinal that bounds the cardinality of the index type and all components also
+bounds the cardinality of the direct limit. -/
+theorem mk_le_of_aleph0_le (c : Cardinal.{max u v}) (hc : ℵ₀ ≤ c)
+    (hι : Cardinal.lift.{v} #ι ≤ c) (hF : ∀ i, Cardinal.lift.{u} #(F i) ≤ c) :
+    #(DirectLimit F (f · · ·)) ≤ c :=
+  (mk_le_sum f).trans <| (sum_le_lift_mk_mul_iSup_lift _).trans <|
+    Cardinal.mul_le_of_le hc hι (ciSup_le' hF)
+
+/-- If all canonical maps into a direct limit are injective, then the supremum of the
+cardinalities of the components is at most the cardinality of the direct limit. -/
+theorem iSup_lift_mk_le_mk
+    (h : ∀ i, Injective fun x ↦ (⟦⟨i, x⟩⟧ : DirectLimit F (f · · ·))) :
+    (⨆ i, Cardinal.lift.{u} #(F i)) ≤ #(DirectLimit F (f · · ·)) := by
+  refine ciSup_le' fun i ↦ ?_
+  have := lift_mk_le_lift_mk_of_injective (h i)
+  simp [DirectLimit]
+  rwa [Cardinal.lift_umax, Cardinal.lift_id'.{v,u}] at this
+
+/-- If all canonical maps into a direct limit are injective and the supremum of the component
+cardinalities is greater than the cardinality of the index type, then it equals the cardinality
+of the direct limit. -/
+theorem mk_eq_iSup_lift_mk
+    (hι : Cardinal.lift.{v} #ι ≤ ⨆ i, Cardinal.lift.{u} #(F i))
+    (h : ∀ i, Injective fun x ↦ (⟦⟨i, x⟩⟧ : DirectLimit F (f · · ·))) :
+    #(DirectLimit F (f · · ·)) = ⨆ i, Cardinal.lift.{u} #(F i) := by
+  refine le_antisymm ?_ (iSup_lift_mk_le_mk f h)
+  by_cases! hc : ℵ₀ ≤ ⨆ i, lift.{u, v} #(F i)
+  · exact mk_le_of_aleph0_le f _ hc hι fun i ↦ le_ciSup Cardinal.bddAbove_of_small i
+  · haveI : Finite ι := mk_lt_aleph0_iff.mp (lift_lt_aleph0.mp (hι.trans_lt hc))
+    cases isEmpty_or_nonempty ι with
+    | inl hle =>
+      simp
+    | inr hlne =>
+      obtain ⟨m, hm⟩ := Finite.exists_le (id : ι → ι)
+      have he := (equivOfForallLE f m hm).lift_cardinal_eq
+      rw [Cardinal.lift_id'.{v,u}, Cardinal.lift_umax.{v,u}] at he
+      rw [he]
+      exact le_ciSup Cardinal.bddAbove_of_small m
+
+/-- If all components have the same cardinality `c`, the cardinality of the index type is at most
+`c`, and all canonical maps are injective, then the direct limit also has cardinality `c`. -/
+theorem mk_eq_of_forall_lift_mk_eq [Nonempty ι] (c : Cardinal.{max u v})
+    (hι : Cardinal.lift.{v} #ι ≤ c) (hF : ∀ i, Cardinal.lift.{u} #(F i) = c)
+    (h : ∀ i, Injective fun x ↦ (⟦⟨i, x⟩⟧ : DirectLimit F (f · · ·))) :
+    #(DirectLimit F (f · · ·)) = c := by
+  simpa only [hF, ciSup_const] using
+    mk_eq_iSup_lift_mk f (by simpa only [hF, ciSup_const]) h
+
+end DirectLimit

From 2a7d05278d572924c2e9bb675daf6bdca6b7cc54 Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Thu, 23 Jul 2026 19:37:26 +0800
Subject: [PATCH 06/11] feat(ModelTheory/DirectLimit): bound cardinality of
 direct limits

---
 Mathlib/ModelTheory/DirectLimit.lean | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean
index 49e15117d7682a..68fd86f6186c5e 100644
--- a/Mathlib/ModelTheory/DirectLimit.lean
+++ b/Mathlib/ModelTheory/DirectLimit.lean
@@ -164,6 +164,33 @@ namespace DirectLimit
 
 variable [IsDirectedOrder ι] [DirectedSystem G fun i j h => f i j h]
 
+open scoped Cardinal
+
+/-- The cardinality of a direct limit is at most the cardinality of the sigma type of its
+components. -/
+theorem mk_le_mk_sigma :
+    #(DirectLimit G f) ≤ #(Σ i, G i) :=
+  Cardinal.mk_quotient_le
+
+/-- The cardinality of a direct limit is at most the cardinality of the index type times the
+supremum of the cardinalities of its components. -/
+theorem mk_le_lift_mk_mul_iSup_lift_mk :
+    #(DirectLimit G f) ≤
+      Cardinal.lift.{w} #ι * ⨆ i, Cardinal.lift.{v} #(G i) := by
+  apply (mk_le_mk_sigma G f).trans
+  rw [Cardinal.mk_sigma]
+  exact Cardinal.sum_le_lift_mk_mul_iSup_lift _
+
+/-- If the index type and all components have cardinality at most an infinite cardinal `κ`, then
+so does the direct limit. -/
+theorem mk_le_of_lift_mk_le {κ : Cardinal.{max v w}}
+    (hκ : ℵ₀ ≤ κ) (hι : Cardinal.lift.{w} #ι ≤ κ)
+    (hG : ∀ i, Cardinal.lift.{v} #(G i) ≤ κ) :
+    #(DirectLimit G f) ≤ κ := by
+  apply (mk_le_lift_mk_mul_iSup_lift_mk G f).trans
+  apply (mul_le_mul' hι (ciSup_le' hG)).trans
+  rw [Cardinal.mul_eq_self hκ]
+
 theorem equiv_iff {x y : Σˣ f} {i : ι} (hx : x.1 ≤ i) (hy : y.1 ≤ i) :
     x ≈ y ↔ (f x.1 i hx) x.2 = (f y.1 i hy) y.2 := by
   cases x

From 82ea7d79b08dda5477c8f70b098344ba3a3f0717 Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Thu, 23 Jul 2026 20:18:09 +0800
Subject: [PATCH 07/11] feat(ModelTheory): add elementary chains

---
 Mathlib.lean                             |   1 +
 Mathlib/ModelTheory/ElementaryChain.lean | 258 +++++++++++++++++++++++
 2 files changed, 259 insertions(+)
 create mode 100644 Mathlib/ModelTheory/ElementaryChain.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 2926f132d98b81..d5c33f8be66cd4 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5700,6 +5700,7 @@ public import Mathlib.ModelTheory.Bundled
 public import Mathlib.ModelTheory.Complexity
 public import Mathlib.ModelTheory.Definability
 public import Mathlib.ModelTheory.DirectLimit
+public import Mathlib.ModelTheory.ElementaryChain
 public import Mathlib.ModelTheory.ElementaryMaps
 public import Mathlib.ModelTheory.ElementarySubstructures
 public import Mathlib.ModelTheory.Encoding
diff --git a/Mathlib/ModelTheory/ElementaryChain.lean b/Mathlib/ModelTheory/ElementaryChain.lean
new file mode 100644
index 00000000000000..0f776b45636533
--- /dev/null
+++ b/Mathlib/ModelTheory/ElementaryChain.lean
@@ -0,0 +1,258 @@
+/-
+Copyright (c) 2026 Zikang Yu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zikang Yu
+-/
+module
+
+public import Mathlib.ModelTheory.DirectLimit
+public import Mathlib.ModelTheory.ElementaryMaps
+
+/-!
+# Elementary chains
+
+This file defines elementary chains without choosing a common ambient structure. Their unions are
+constructed as direct limits of the underlying directed systems of first-order embeddings.
+
+## Main definitions
+
+- `FirstOrder.Language.ElementaryChain`: A system of structures whose transition maps are
+  elementary embeddings.
+- `FirstOrder.Language.ElementaryChain.ofNatSucc`: The elementary chain generated by a sequence of
+  elementary embeddings between successive stages.
+- `FirstOrder.Language.ElementaryChain.Limit`: The direct limit of an elementary chain.
+- `FirstOrder.Language.ElementaryChain.toLimitElementary`: The canonical elementary embedding of a
+  stage into the limit.
+- `FirstOrder.Language.ElementaryChain.liftElementary`: The elementary lift of a compatible
+  cocone.
+
+## Main results
+
+- `FirstOrder.Language.ElementaryChain.realize_toLimit`: Bounded formulas are preserved and
+  reflected by the canonical maps into the limit.
+- `FirstOrder.Language.ElementaryChain.limit_models`: A theory modeled by a stage is modeled by the
+  limit.
+-/
+
+@[expose] public section
+
+universe u v w w'
+
+namespace FirstOrder
+
+namespace Language
+
+open scoped Cardinal
+
+/-- A system of `L`-structures whose transition maps are elementary embeddings. -/
+structure ElementaryChain (L : Language.{u, v}) (ι : Type w) [Preorder ι] where
+  carrier : ι → Type w'
+  [struc : ∀ i, L.Structure (carrier i)]
+  map : ∀ i j, i ≤ j → carrier i ↪ₑ[L] carrier j
+  map_self : ∀ i x, map i i le_rfl x = x
+  map_map : ∀ i j k (hij : i ≤ j) (hjk : j ≤ k) (x : carrier i),
+    map j k hjk (map i j hij x) = map i k (hij.trans hjk) x
+
+attribute [instance] ElementaryChain.struc
+
+namespace ElementaryEmbedding
+
+variable {L : Language.{u, v}} {M : ℕ → Type w'} [∀ n, L.Structure (M n)]
+
+/-- Compose a sequence of elementary embeddings along an interval of natural numbers. -/
+noncomputable def natLERec (f : ∀ n, M n ↪ₑ[L] M (n + 1))
+    (m n : ℕ) (h : m ≤ n) : M m ↪ₑ[L] M n :=
+  Nat.leRecOn h (@fun k g ↦ (f k).comp g) (refl L _)
+
+private theorem coe_natLERec (f : ∀ n, M n ↪ₑ[L] M (n + 1))
+    (m n : ℕ) (h : m ≤ n) :
+    (natLERec f m n h : M m → M n) =
+      DirectedSystem.natLERec (fun n ↦ (f n).toEmbedding) m n h := by
+  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
+  ext x
+  induction k with
+  | zero => simp [natLERec, DirectedSystem.natLERec, Nat.leRecOn_self]
+  | succ k ih =>
+    simp only [natLERec, DirectedSystem.coe_natLERec]
+    rw [Nat.leRecOn_succ le_self_add, Nat.leRecOn_succ le_self_add]
+    specialize ih (Nat.le_add_right m k)
+    simp only [natLERec, DirectedSystem.coe_natLERec] at ih
+    exact congrArg (f (m + k)) ih
+
+/-- Iterated composition over a reflexive natural-number interval is the identity. -/
+@[simp]
+theorem natLERec_self (f : ∀ n, M n ↪ₑ[L] M (n + 1)) (n : ℕ) (x : M n) :
+    natLERec f n n le_rfl x = x := by
+  simp [natLERec, Nat.leRecOn_self]
+
+/-- Iterated composition over one successor step is the supplied elementary embedding. -/
+@[simp]
+theorem natLERec_succ (f : ∀ n, M n ↪ₑ[L] M (n + 1)) (n : ℕ) (x : M n) :
+    natLERec f n (n + 1) (Nat.le_succ n) x = f n x := by
+  simp [natLERec, Nat.leRecOn]
+
+/-- Iterated elementary embeddings compose coherently across adjacent intervals. -/
+theorem natLERec_trans {f : ∀ n, M n ↪ₑ[L] M (n + 1)}
+    {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) (x : M i) :
+    natLERec f j k hjk (natLERec f i j hij x) = natLERec f i k (hij.trans hjk) x := by
+  simpa only [coe_natLERec] using
+    DirectedSystem.map_map
+      (fun i j h ↦ DirectedSystem.natLERec (fun n ↦ (f n).toEmbedding) i j h) hij hjk x
+
+end ElementaryEmbedding
+
+namespace ElementaryChain
+
+variable {L : Language.{u, v}} {ι : Type w} [Preorder ι]
+
+/-- Construct a countable elementary chain by composing elementary embeddings between successive
+stages. -/
+noncomputable def ofNatSucc (M : ℕ → Type w') [∀ n, L.Structure (M n)]
+    (f : ∀ n, M n ↪ₑ[L] M (n + 1)) : ElementaryChain L ℕ where
+  carrier := M
+  map := ElementaryEmbedding.natLERec f
+  map_self := ElementaryEmbedding.natLERec_self f
+  map_map := fun _ _ _ hij hjk x ↦ ElementaryEmbedding.natLERec_trans hij hjk x
+
+/-- The transition map of `ofNatSucc` between successive stages is the supplied elementary
+embedding. -/
+@[simp]
+theorem ofNatSucc_map_succ (M : ℕ → Type w') [∀ n, L.Structure (M n)]
+    (f : ∀ n, M n ↪ₑ[L] M (n + 1)) (n : ℕ) :
+    (ofNatSucc M f).map n (n + 1) (Nat.le_succ n) = f n := by
+  ext x
+  exact ElementaryEmbedding.natLERec_succ f n x
+
+/-- The underlying first-order embeddings form a directed system. -/
+instance toEmbeddingDirectedSystem (C : ElementaryChain L ι) :
+    DirectedSystem C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) where
+  map_self i x := C.map_self i x
+  map_map k j i hij hjk x := C.map_map i j k hij hjk x
+
+variable [IsDirectedOrder ι]
+
+/-- The abstract union of an elementary chain, constructed without an ambient structure. -/
+abbrev Limit (C : ElementaryChain L ι) :=
+  L.DirectLimit C.carrier (fun i j h ↦ (C.map i j h).toEmbedding)
+
+variable [Nonempty ι]
+
+/-- The canonical first-order embedding of a stage into the direct limit. -/
+noncomputable def toLimit (C : ElementaryChain L ι) (i : ι) : C.carrier i ↪[L] C.Limit :=
+  DirectLimit.of L ι C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) i
+
+/-- The canonical maps commute with the transition maps. -/
+@[simp]
+theorem toLimit_map (C : ElementaryChain L ι) {i j : ι} (hij : i ≤ j) (x : C.carrier i) :
+    C.toLimit j (C.map i j hij x) = C.toLimit i x := by
+  unfold toLimit
+  exact DirectLimit.of_f
+
+/-- Every element of the direct limit is represented by an element of some stage. -/
+theorem exists_toLimit (C : ElementaryChain L ι) (z : C.Limit) :
+    ∃ (i : ι) (x : C.carrier i), C.toLimit i x = z := by
+  simpa [toLimit] using DirectLimit.exists_of z
+
+omit [Nonempty ι] in
+theorem mk_limit_le_mk_sigma (C : ElementaryChain L ι) :
+    #(C.Limit) ≤ #(Σ i, C.carrier i) :=
+  DirectLimit.mk_le_mk_sigma C.carrier fun i j h ↦ (C.map i j h).toEmbedding
+
+omit [Nonempty ι] in
+theorem mk_limit_le_lift_mk_mul_iSup_lift_mk (C : ElementaryChain L ι) :
+    #(C.Limit) ≤ Cardinal.lift.{w'} #ι * ⨆ i, Cardinal.lift.{w} #(C.carrier i) :=
+  DirectLimit.mk_le_lift_mk_mul_iSup_lift_mk C.carrier
+    fun i j h ↦ (C.map i j h).toEmbedding
+
+omit [Nonempty ι] in
+theorem mk_limit_le_of_lift_mk_le (C : ElementaryChain L ι) {κ : Cardinal.{max w w'}}
+    (hκ : ℵ₀ ≤ κ) (hι : Cardinal.lift.{w'} #ι ≤ κ)
+    (hC : ∀ i, Cardinal.lift.{w} #(C.carrier i) ≤ κ) :
+    #(C.Limit) ≤ κ :=
+  DirectLimit.mk_le_of_lift_mk_le C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) hκ hι hC
+
+/-- Realization of bounded formulas is preserved and reflected by a canonical map into the direct
+limit. -/
+theorem realize_toLimit (C : ElementaryChain L ι) {α : Type*} {n : ℕ}
+    (φ : L.BoundedFormula α n) (i : ι) (v : α → C.carrier i)
+    (xs : Fin n → C.carrier i) :
+    φ.Realize (C.toLimit i ∘ v) (C.toLimit i ∘ xs) ↔ φ.Realize v xs := by
+  induction φ generalizing i with
+  | falsum => rfl
+  | equal t₁ t₂ =>
+    simp [BoundedFormula.Realize, ← Sum.comp_elim]
+  | rel R ts =>
+    simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]
+    exact StrongHomClass.map_rel (C.toLimit i) R
+      (fun i ↦ Term.realize (Sum.elim v xs) (ts i))
+  | imp φ ψ ihφ ihψ =>
+    simp [BoundedFormula.Realize, ihφ, ihψ]
+  | @all n φ ih =>
+    simp only [BoundedFormula.realize_all, Nat.succ_eq_add_one]
+    constructor <;> intro h x
+    · simpa [← Fin.comp_snoc, ih i v (Fin.snoc xs x)] using h (C.toLimit i x)
+    · obtain ⟨j, xj, rfl⟩ := C.exists_toLimit x
+      obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j
+      rw [← BoundedFormula.Realize,
+        ← (C.map i k hik).map_boundedFormula φ.all v xs, BoundedFormula.Realize] at h
+      specialize h (C.map j k hjk xj)
+      specialize ih k (C.map i k hik ∘ v)
+        (Fin.snoc (C.map i k hik ∘ xs) (C.map j k hjk xj))
+      rw [← ih, Fin.comp_snoc] at h
+      convert h using 1 <;> simp [Function.comp_def, C.toLimit_map]
+
+/-- The canonical map from each stage to the direct limit is elementary. -/
+noncomputable def toLimitElementary (C : ElementaryChain L ι) (i : ι) :
+    C.carrier i ↪ₑ[L] C.Limit where
+  toFun := C.toLimit i
+  map_formula' := fun n φ v ↦ by
+    change BoundedFormula.Realize φ (C.toLimit i ∘ v) default ↔
+      BoundedFormula.Realize φ v default
+    convert C.realize_toLimit φ i v default
+
+/-- A finite family of elements of the direct limit can be lifted to a common stage of the chain.
+-/
+theorem exists_finite_common_stage (C : ElementaryChain L ι) {α : Type*} [Finite α]
+    (x : α → C.Limit) : ∃ (i : ι) (z : α → C.carrier i), C.toLimit i ∘ z = x := by
+  obtain ⟨i, z, hz⟩ := DirectLimit.exists_quotient_mk'_sigma_mk'_eq C.carrier
+    (fun i j h ↦ (C.map i j h).toEmbedding) x
+  exact ⟨i, z, by simpa [toLimit, Function.comp_def] using hz.symm⟩
+
+/-- A compatible cocone of elementary embeddings induces an elementary embedding from the direct
+limit. This is the elementary version of `Language.DirectLimit.lift`. -/
+noncomputable def liftElementary (C : ElementaryChain L ι) {P : Type*} [L.Structure P]
+    (g : ∀ i, C.carrier i ↪ₑ[L] P)
+    (comm : ∀ i j (hij : i ≤ j) (x : C.carrier i), g j (C.map i j hij x) = g i x) :
+    C.Limit ↪ₑ[L] P :=
+  let F : C.Limit ↪[L] P := Language.DirectLimit.lift L ι C.carrier
+    (fun i j h ↦ (C.map i j h).toEmbedding)
+    (fun i ↦ (g i).toEmbedding)
+    (by intro i j hij x; simpa using comm i j hij x)
+  { toFun := F
+    map_formula' := by
+      intro n φ x
+      obtain ⟨i, z, hz⟩ := C.exists_finite_common_stage x
+      have hF_lift : ∀ a : C.carrier i, F (C.toLimit i a) = g i a := by
+        intro a
+        simp [F, toLimit]
+      have h_eq : F ∘ x = (g i : C.carrier i → P) ∘ z := by
+        ext k
+        calc
+          F (x k) = F (C.toLimit i (z k)) := by simp [← hz]
+          _ = g i (z k) := hF_lift (z k)
+      rw [h_eq]
+      exact ((g i).map_formula' φ z).trans <| by
+        rw [← hz]
+        exact ((C.toLimitElementary i).map_formula' φ z).symm }
+
+/-- If some stage is a model of `T`, then the direct limit is also a model of `T`. -/
+theorem limit_models (C : ElementaryChain L ι) (T : L.Theory)
+    (hT : ∃ i, C.carrier i ⊨ T) : C.Limit ⊨ T := by
+  obtain ⟨i, hi⟩ := hT
+  exact ((C.toLimitElementary i).theory_model_iff T).1 hi
+
+end ElementaryChain
+
+end Language
+
+end FirstOrder

From 11279a19080c834f59946f2e305551f28464751b Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Thu, 23 Jul 2026 20:52:59 +0800
Subject: [PATCH 08/11] add docstings to fix lint

---
 Mathlib/ModelTheory/ElementaryChain.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/ModelTheory/ElementaryChain.lean b/Mathlib/ModelTheory/ElementaryChain.lean
index 0f776b45636533..ad2a511d59217c 100644
--- a/Mathlib/ModelTheory/ElementaryChain.lean
+++ b/Mathlib/ModelTheory/ElementaryChain.lean
@@ -46,8 +46,10 @@ open scoped Cardinal
 
 /-- A system of `L`-structures whose transition maps are elementary embeddings. -/
 structure ElementaryChain (L : Language.{u, v}) (ι : Type w) [Preorder ι] where
+  /-- The structure at each stage of the chain. -/
   carrier : ι → Type w'
   [struc : ∀ i, L.Structure (carrier i)]
+  /-- The elementary embedding from stage `i` to stage `j` when `i ≤ j`. -/
   map : ∀ i j, i ≤ j → carrier i ↪ₑ[L] carrier j
   map_self : ∀ i x, map i i le_rfl x = x
   map_map : ∀ i j k (hij : i ≤ j) (hjk : j ≤ k) (x : carrier i),

From 4e79d30deeaa4a88816bdc11e3f9d9473591fe78 Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Mon, 27 Jul 2026 14:16:18 +0800
Subject: [PATCH 09/11] refactor: reuse direct limit cardinality bounds

---
 Mathlib/ModelTheory/DirectLimit.lean     | 27 -------------------
 Mathlib/ModelTheory/ElementaryChain.lean | 33 +++++++++++++++---------
 2 files changed, 21 insertions(+), 39 deletions(-)

diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean
index 68fd86f6186c5e..49e15117d7682a 100644
--- a/Mathlib/ModelTheory/DirectLimit.lean
+++ b/Mathlib/ModelTheory/DirectLimit.lean
@@ -164,33 +164,6 @@ namespace DirectLimit
 
 variable [IsDirectedOrder ι] [DirectedSystem G fun i j h => f i j h]
 
-open scoped Cardinal
-
-/-- The cardinality of a direct limit is at most the cardinality of the sigma type of its
-components. -/
-theorem mk_le_mk_sigma :
-    #(DirectLimit G f) ≤ #(Σ i, G i) :=
-  Cardinal.mk_quotient_le
-
-/-- The cardinality of a direct limit is at most the cardinality of the index type times the
-supremum of the cardinalities of its components. -/
-theorem mk_le_lift_mk_mul_iSup_lift_mk :
-    #(DirectLimit G f) ≤
-      Cardinal.lift.{w} #ι * ⨆ i, Cardinal.lift.{v} #(G i) := by
-  apply (mk_le_mk_sigma G f).trans
-  rw [Cardinal.mk_sigma]
-  exact Cardinal.sum_le_lift_mk_mul_iSup_lift _
-
-/-- If the index type and all components have cardinality at most an infinite cardinal `κ`, then
-so does the direct limit. -/
-theorem mk_le_of_lift_mk_le {κ : Cardinal.{max v w}}
-    (hκ : ℵ₀ ≤ κ) (hι : Cardinal.lift.{w} #ι ≤ κ)
-    (hG : ∀ i, Cardinal.lift.{v} #(G i) ≤ κ) :
-    #(DirectLimit G f) ≤ κ := by
-  apply (mk_le_lift_mk_mul_iSup_lift_mk G f).trans
-  apply (mul_le_mul' hι (ciSup_le' hG)).trans
-  rw [Cardinal.mul_eq_self hκ]
-
 theorem equiv_iff {x y : Σˣ f} {i : ι} (hx : x.1 ≤ i) (hy : y.1 ≤ i) :
     x ≈ y ↔ (f x.1 i hx) x.2 = (f y.1 i hy) y.2 := by
   cases x
diff --git a/Mathlib/ModelTheory/ElementaryChain.lean b/Mathlib/ModelTheory/ElementaryChain.lean
index ad2a511d59217c..ee99dec227fa2a 100644
--- a/Mathlib/ModelTheory/ElementaryChain.lean
+++ b/Mathlib/ModelTheory/ElementaryChain.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.ModelTheory.DirectLimit
 public import Mathlib.ModelTheory.ElementaryMaps
+public import Mathlib.SetTheory.Cardinal.DirectLimit
 
 /-!
 # Elementary chains
@@ -155,23 +156,31 @@ theorem exists_toLimit (C : ElementaryChain L ι) (z : C.Limit) :
     ∃ (i : ι) (x : C.carrier i), C.toLimit i x = z := by
   simpa [toLimit] using DirectLimit.exists_of z
 
-omit [Nonempty ι] in
-theorem mk_limit_le_mk_sigma (C : ElementaryChain L ι) :
-    #(C.Limit) ≤ #(Σ i, C.carrier i) :=
-  DirectLimit.mk_le_mk_sigma C.carrier fun i j h ↦ (C.map i j h).toEmbedding
-
-omit [Nonempty ι] in
-theorem mk_limit_le_lift_mk_mul_iSup_lift_mk (C : ElementaryChain L ι) :
-    #(C.Limit) ≤ Cardinal.lift.{w'} #ι * ⨆ i, Cardinal.lift.{w} #(C.carrier i) :=
-  DirectLimit.mk_le_lift_mk_mul_iSup_lift_mk C.carrier
-    fun i j h ↦ (C.map i j h).toEmbedding
+private def limitEquiv (C : ElementaryChain L ι) :
+    C.Limit ≃
+      _root_.DirectLimit C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) :=
+  Quotient.congrRight fun _ _ ↦ Iff.rfl
 
 omit [Nonempty ι] in
+/-- An infinite cardinal bounding the index type and every stage also bounds the limit. -/
 theorem mk_limit_le_of_lift_mk_le (C : ElementaryChain L ι) {κ : Cardinal.{max w w'}}
     (hκ : ℵ₀ ≤ κ) (hι : Cardinal.lift.{w'} #ι ≤ κ)
     (hC : ∀ i, Cardinal.lift.{w} #(C.carrier i) ≤ κ) :
-    #(C.Limit) ≤ κ :=
-  DirectLimit.mk_le_of_lift_mk_le C.carrier (fun i j h ↦ (C.map i j h).toEmbedding) hκ hι hC
+    #(C.Limit) ≤ κ := by
+  rw [(limitEquiv C).cardinal_eq]
+  exact _root_.DirectLimit.mk_le_of_aleph0_le
+    (fun i j h ↦ (C.map i j h).toEmbedding) κ hκ hι hC
+
+/-- If every stage has cardinality `κ` and the index type has cardinality at most `κ`, then the
+limit also has cardinality `κ`. -/
+theorem mk_limit_eq_of_forall_lift_mk_eq (C : ElementaryChain L ι)
+    (κ : Cardinal.{max w w'}) (hι : Cardinal.lift.{w'} #ι ≤ κ)
+    (hC : ∀ i, Cardinal.lift.{w} #(C.carrier i) = κ) :
+    #(C.Limit) = κ := by
+  rw [(limitEquiv C).cardinal_eq]
+  apply _root_.DirectLimit.mk_eq_of_forall_lift_mk_eq
+    (fun i j h ↦ (C.map i j h).toEmbedding) κ hι hC
+  exact _root_.DirectLimit.mk_injective _ fun i j h ↦ (C.map i j h).injective
 
 /-- Realization of bounded formulas is preserved and reflected by a canonical map into the direct
 limit. -/

From e3821a10c3423180d7a2405f502aea25bd2491bf Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Tue, 28 Jul 2026 21:26:53 +0800
Subject: [PATCH 10/11] feat(ModelTheory): construct a counterexample to the
 two-cardinal phenomenon

---
 Mathlib.lean                           |   1 +
 Mathlib/ModelTheory/DefinablyFull.lean | 405 +++++++++++++++++++++++++
 Mathlib/ModelTheory/Encoding.lean      |  33 ++
 Mathlib/ModelTheory/LanguageMap.lean   |  27 ++
 4 files changed, 466 insertions(+)
 create mode 100644 Mathlib/ModelTheory/DefinablyFull.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index d5c33f8be66cd4..abd7477faa9c6a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5699,6 +5699,7 @@ public import Mathlib.ModelTheory.Basic
 public import Mathlib.ModelTheory.Bundled
 public import Mathlib.ModelTheory.Complexity
 public import Mathlib.ModelTheory.Definability
+public import Mathlib.ModelTheory.DefinablyFull
 public import Mathlib.ModelTheory.DirectLimit
 public import Mathlib.ModelTheory.ElementaryChain
 public import Mathlib.ModelTheory.ElementaryMaps
diff --git a/Mathlib/ModelTheory/DefinablyFull.lean b/Mathlib/ModelTheory/DefinablyFull.lean
new file mode 100644
index 00000000000000..9bb838d6d14f8c
--- /dev/null
+++ b/Mathlib/ModelTheory/DefinablyFull.lean
@@ -0,0 +1,405 @@
+/-
+Copyright (c) 2026 NoneMore. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: NoneMore
+-/
+module
+
+public import Mathlib.ModelTheory.Definability
+public import Mathlib.ModelTheory.ElementaryChain
+public import Mathlib.ModelTheory.LanguageMap
+public import Mathlib.ModelTheory.Satisfiability
+
+/-!
+# Definably full structures
+
+This file constructs large models in which every parameter-definable unary set is either finite or
+has the same cardinality as the model.
+
+## Main definitions
+
+- `FirstOrder.Language.UnaryDefinablyFull`: Every infinite parameter-definable unary set has the
+  cardinality of the ambient structure.
+- `FirstOrder.Language.DefinablyFull`: Every infinite parameter-definable finite-arity set has the
+  cardinality of the ambient structure.
+
+## Main results
+
+- `FirstOrder.Language.Theory.exists_elementaryExtension_card_eq_with_full_unary_realizations`
+  constructs a one-step elementary extension fully realizing every infinite unary formula over the
+  base model.
+- `FirstOrder.Language.Theory.exists_model_of_card_definably_full` constructs a definably full
+  model of any prescribed infinite cardinality in a countable language.
+-/
+
+@[expose] public section
+
+universe u v w z
+
+namespace FirstOrder
+
+namespace Language
+
+open scoped Cardinal
+
+/-- Every infinite unary set definable with parameters from `A` has the cardinality of `M`. -/
+def UnaryDefinablyFull
+    (L : Language.{u, v}) (M : Type w) [L.Structure M] : Prop :=
+  ∀ (A X : Set M), A.Definable₁ L X → X.Infinite → #X = #M
+
+/-- Every infinite finite-arity set definable with parameters from `A` has the cardinality of
+`M`. -/
+def DefinablyFull (L : Language.{u, v}) (M : Type w) [L.Structure M] : Prop :=
+  ∀ (A : Set M) {n : ℕ} (S : Set (Fin n → M)), A.Definable L S → S.Infinite → #S = #M
+
+/-- A structure is definably full if it is unary definably full. -/
+theorem definablyFull_of_unary
+    {L : Language.{u, v}} {M : Type w} [L.Structure M] [Infinite M]
+    (h : UnaryDefinablyFull L M) :
+    DefinablyFull L M := by
+  simp only [UnaryDefinablyFull, DefinablyFull] at ⊢ h
+  intro A n S hSD hSI
+  let P (i : Fin n) := (fun x : Fin n → M ↦ x i) '' S
+  have hP : ∃ i : Fin n, (P i).Infinite := by
+    contrapose! hSI
+    exact Set.forall_finite_image_eval_iff.mp hSI
+  rcases hP with ⟨i, hPiI⟩
+  have hPiD : A.Definable₁ L (P i) := by
+    simp only [P, Set.Definable₁]
+    convert hSD.image_comp fun _ : Fin 1 ↦ i
+    ext x
+    simp [funext_iff]
+  specialize h A (P i) hPiD hPiI
+  apply le_antisymm
+  · trans #(Fin n → M)
+    · exact Cardinal.mk_set_le S
+    · rw [Cardinal.mk_pi, Cardinal.prod_const]
+      simpa using Cardinal.power_nat_le (Cardinal.aleph0_le_mk M)
+  · simpa [← h] using Cardinal.mk_image_le
+
+namespace Formula
+
+variable {L : Language.{u, v}} {M : Type*} [L.Structure M]
+
+/-- Unary realizations indexed by `Fin 1` are equivalent to their underlying elements. -/
+def finOneRealizationsEquiv (φ : L.Formula (Fin 1)) :
+    {x : Fin 1 → M | φ.Realize x} ≃ {x : M | φ.Realize fun _ ↦ x} := by
+  refine (Equiv.funUnique (Fin 1) M).subtypeEquiv ?_
+  intro v
+  simp only [Set.mem_ofPred_eq, Equiv.funUnique_apply, Fin.default_eq_zero, Fin.isValue]
+  congr!
+
+end Formula
+
+namespace Theory
+
+open Cardinal Set
+
+variable {L : Language.{u, v}} (T : L.Theory)
+
+/-- Given a model `M` of cardinality `κ`, constructs an elementary extension `N` of cardinality
+`κ` in which every infinite unary formula with parameters in `M` has `κ` realizations. -/
+theorem exists_elementaryExtension_card_eq_with_full_unary_realizations
+    {κ : Cardinal.{w}} (M : ModelType.{u, v, w} T) (hM : #M = κ)
+    (hκ : ℵ₀ ≤ κ) (hL : Cardinal.lift.{w} L.card ≤ Cardinal.lift.{max u v} κ) :
+    ∃ (N : ModelType.{u, v, w} T) (e : M ↪ₑ[L] N),
+      #N = κ ∧
+        ∀ {β : Type z} (ψ : L.Formula (β ⊕ Fin 1)) (b : β → M),
+          Set.Infinite {x : Fin 1 → M | ψ.Realize (Sum.elim b x)} →
+            #({x : Fin 1 → N | ψ.Realize (Sum.elim (e ∘ b) x)}) = κ := by
+  classical
+  /-
+  For each infinite unary formula over `M`, add `κ` many constants intended to be distinct
+  realizations of that formula.
+  -/
+  let F := {φ : L[[M]].Formula (Fin 1) // Set.Infinite {x : M | φ.Realize fun _ ↦ x}}
+  have hFcard : #F ≤ Cardinal.lift.{max u v} κ := (Cardinal.mk_subtype_le _).trans <|
+    Formula.card_le_withConstants.trans <| by
+      simpa [hM] using
+        ⟨hκ, add_le_of_le (aleph0_le_lift.mpr hκ)
+          (one_le_lift_iff.mpr (one_le_aleph0.trans hκ))
+          (add_le_of_le (aleph0_le_lift.mpr hκ) hL le_rfl)⟩
+  let I := κ.out
+  let fL := L[[M]].lhomWithConstants (F × I)
+  let L' := L[[M]][[F × I]]
+  have hL'card : Cardinal.lift.{w} L'.card ≤ Cardinal.lift.{max u v w} κ := by
+    simp only [card_withConstants, lift_id, mk_prod, lift_add, lift_lift, lift_mul, L']
+    rw [Cardinal.lift_id'.{w, max u v}, Cardinal.lift_umax.{w, max u v}]
+    have hκ' := aleph0_le_lift.mpr hκ
+    exact add_le_of_le hκ' (add_le_of_le hκ' hL (le_of_eq (congrArg _ hM)))
+      (mul_le_of_le hκ' hFcard (by simp [I]))
+  let subst : F → I → L[[M]][[F × I]].Sentence :=
+    fun φ i ↦ (fL.onFormula φ.1).subst (fun _ ↦ (L[[M]].con (φ, i)).term)
+  let T₁ := fL.onTheory (L.elementaryDiagram M)
+  let T₂ (S : Set (F × I)) := (fun p : F × I ↦ subst p.1 p.2) '' S
+  let T₃ (S : Set (F × I)) :=
+    ⋃ φ : F, L[[M]].distinctConstantsTheory (S ∩ {p : F × I | p.1 = φ})
+  let Γ (s : Finset (F × I)) : L'.Theory := T₁ ∪ T₂ s ∪ T₃ s
+  /-
+  A finite fragment is satisfiable in `M`: for each formula occurring in the fragment, assign
+  its finitely many new constants to distinct elements of its infinite realization set.
+  -/
+  have hΓ (s : Finset (F × I)) : (Γ s).IsSatisfiable := by
+    let sφi (φ : F) : Finset I := ({v : F × I | v ∈ s ∧ v.1 = φ}.image Prod.snd).toFinset
+    have hsφi : ∀ v ∈ s, v.2 ∈ sφi v.1 := by simp [sφi]
+    let rs : F → Set M := fun φ ↦ {x | φ.1.Realize fun _ ↦ x}
+    have hrs (φ : F) : (rs φ).Infinite := φ.2
+    let valOn : s → M := fun v ↦ by
+      let f := (hrs v.1.1).natEmbedding
+      let n := (sφi v.1.1).equivFin ⟨v.1.2, hsφi v v.2⟩ |>.toNat
+      exact (f n).1
+    have hrealize (v : s) : v.1.1.1.Realize fun _ ↦ valOn v := by
+      change valOn v ∈ rs v.1.1
+      simp [valOn, rs]
+    have hdistinct (φ : F) (i j : I) (hi : (φ, i) ∈ s) (hj : (φ, j) ∈ s)
+        (hval : valOn ⟨(φ, i), hi⟩ = valOn ⟨(φ, j), hj⟩) : i = j := by
+      simp only [Fin.toNat_eq_val, valOn] at hval
+      exact Subtype.ext_iff.mp <| (sφi φ).equivFin.injective <|
+        Fin.ext <| (hrs φ).natEmbedding.injective (Subtype.ext hval)
+    letI : Inhabited M := Classical.inhabited_of_nonempty inferInstance
+    let val : F × I → M := Function.extend ((↑) : s → F × I) valOn default
+    have hval (v : s) : val v = valOn v := by simp [val]
+    letI : (constantsOn (F × I)).Structure M := constantsOn.structure val
+    have hcon (p : F × I) : (L[[M]].con p : M) = val p := rfl
+    have hT₁ : M ⊨ T₁ :=
+      (LHom.onTheory_model fL (L.elementaryDiagram ↑M)).mpr model_completeTheory
+    have hT₂ : M ⊨ T₂ s := by
+      rw [model_iff]
+      rintro ψ ⟨v, hv, rfl⟩
+      simp only [subst, Sentence.Realize, Formula.Realize, BoundedFormula.realize_subst,
+        Term.realize_constants, hcon, LHom.onFormula]
+      rw [LHom.realize_onBoundedFormula fL]
+      simpa only [Formula.Realize, ← hval] using hrealize ⟨v, hv⟩
+    have hT₃ : M ⊨ T₃ s := by
+      simp only [distinctConstantsTheory, model_iff, mem_iUnion, mem_image, mem_inter_iff, mem_prod,
+        SetLike.mem_coe, mem_ofPred_eq, mem_compl_iff, mem_diagonal_iff, ne_eq, Prod.exists,
+        ↓existsAndEq, and_true, Prod.mk.injEq, not_and, forall_const, forall_exists_index, and_imp,
+        T₃]
+      intro ψ φ i j hi hj hij rfl
+      simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal,
+        Term.realize_constants, hcon]
+      contrapose! hij
+      exact hdistinct φ i j hi hj (by simpa [← hval] using hij)
+    haveI : M ⊨ Γ s := (hT₁.union hT₂).union hT₃
+    exact Model.isSatisfiable M
+  /-
+  The finite theories are directed by inclusion, and their union is the theory containing every
+  realization and distinctness requirement.
+  -/
+  have hΓ' : Directed (· ⊆ ·) Γ :=
+    Monotone.directed_le fun s t hst ↦ by
+      simp only [Γ, T₂, T₃]
+      exact union_subset_union (union_subset_union subset_rfl (image_mono hst))
+        (iUnion_mono fun _ ↦ distinctConstantsTheory_mono
+          (inter_subset_inter hst subset_rfl))
+  let Sigma := T₁ ∪ T₂ univ ∪ T₃ univ
+  have Sigma_eq_iUnion : Sigma = ⋃ s, Γ s := by
+    simp only [Sigma, Γ]
+    rw [Set.iUnion_union_distrib, Set.iUnion_union_distrib, iUnion_const]
+    have hT₂ : T₂ Set.univ = ⋃ s : Finset (F × I), T₂ s := by
+      simp only [image_univ, ← image_iUnion, T₂]
+      rw [Set.iUnion_eq_univ_iff.mpr fun x ↦ ⟨{x}, by simp⟩, image_univ]
+    have hT₃ : T₃ Set.univ = ⋃ s : Finset (F × I), T₃ s := by
+      simp only [univ_inter, T₃]
+      refine subset_antisymm ?_ (iUnion_subset fun s ↦
+        iUnion_mono fun φ ↦ distinctConstantsTheory_mono inter_subset_right)
+      refine iUnion_subset fun φ ↦ ?_
+      rw [distinctConstantsTheory_eq_iUnion]
+      refine iUnion_subset fun s ↦ ?_
+      refine subset_iUnion₂_of_subset
+        (s.map (Function.Embedding.subtype fun p : F × I ↦ p.1 = φ)) φ ?_
+      rw [inter_eq_left.mpr (by
+        simp only [Finset.coe_map, Function.Embedding.subtype_apply, Function.Embedding.coe_subtype,
+          image_subset_iff, preimage_ofPred_eq]
+        exact fun x _ ↦ x.2)]
+      simp
+    simp [hT₂, hT₃]
+  /- Compactness for directed unions now supplies a model of all the requirements at once. -/
+  obtain ⟨P⟩ := Sigma_eq_iUnion ▸ (isSatisfiable_directed_union_iff hΓ').mpr hΓ
+  letI : L[[M]].Structure P := fL.reduct P
+  letI : L.Structure P := (L.lhomWithConstants M).reduct P
+  haveI : P ⊨ L.elementaryDiagram M := (LHom.onTheory_model fL _).mp <|
+    Theory.Model.mono P.is_model fun _ hψ ↦ Or.inl (Or.inl hψ)
+  let eP : M ↪ₑ[L] P := ElementaryEmbedding.ofModelsElementaryDiagram L M P
+  have hPcard : Cardinal.lift.{max u v w} κ ≤ Cardinal.lift.{w} #P :=
+    hM ▸ lift_mk_le'.mpr ⟨eP, eP.injective⟩
+  /-
+  The compactness model may be too large. Downward Löwenheim–Skolem gives an elementary submodel
+  `N` of cardinality `κ`, which still satisfies the whole expanded theory.
+  -/
+  obtain ⟨N, ⟨e'⟩, hNcard⟩ :=
+    L'.exists_elementaryEmbedding_card_eq_of_le P κ hκ hL'card hPcard
+  letI : L[[M]].Structure N := fL.reduct N
+  letI : L.Structure N := (L.lhomWithConstants M).reduct N
+  have hNSigma : N ⊨ Sigma := (e'.theory_model_iff Sigma).mpr P.is_model
+  have hNT₂ : N ⊨ T₂ univ :=
+    Theory.Model.mono hNSigma fun _ hψ ↦ Or.inl (Or.inr hψ)
+  have hNT₃ : N ⊨ T₃ univ := Theory.Model.mono hNSigma fun _ hψ ↦ Or.inr hψ
+  haveI : N ⊨ L.elementaryDiagram M := (LHom.onTheory_model fL _).mp <|
+    Theory.Model.mono hNSigma fun _ hψ ↦ Or.inl (Or.inl hψ)
+  let eN : M ↪ₑ[L] N := ElementaryEmbedding.ofModelsElementaryDiagram L M N
+  haveI : N ⊨ T := (eN.theory_model_iff T).mp (ModelType.is_model M)
+  haveI : Nonempty N := by
+    simpa [← Cardinal.mk_ne_zero_iff, hNcard, ← Cardinal.one_le_iff_ne_zero] using
+      one_le_aleph0.trans hκ
+  haveI : (L.lhomWithConstantsMap ⇑eN).IsExpansionOn ↑N :=
+    LHom.lhomWithConstantsMap_isExpansionOn_of_eq _ fun _ ↦ rfl
+  refine ⟨ModelType.of T N, eN, by simpa, ?_⟩
+  intro β ψ b hψb
+  /-
+  Recode `ψ` with the parameters `b` as a unary formula in the language with constants from `M`.
+  Its realization set is still infinite.
+  -/
+  let φ : L[[M]].Formula (Fin 1) :=
+    BoundedFormula.constantsVarsEquiv.symm (ψ.relabel (Sum.map b id))
+  have hφI : {x : M | φ.Realize fun _ ↦ x}.Infinite := by
+    rw [← infinite_coe_iff, ← φ.finOneRealizationsEquiv.infinite_iff, infinite_coe_iff]
+    convert hψb with v
+    simp only [Formula.Realize, Formula.relabel, ← BoundedFormula.realize_constantsVarsEquiv,
+      _root_.Equiv.apply_symm_apply, BoundedFormula.realize_relabel, Nat.add_zero, Fin.castAdd_zero,
+      Fin.cast_refl, Function.comp_id, Fin.natAdd_zero, φ]
+    congr!
+    ext (_ | _) <;> rfl
+  have hφN :
+      #({x : N | ((L.lhomWithConstantsMap ⇑eN).onFormula φ).Realize fun _ ↦ x}) = κ := by
+    let rsN : Set N :=
+      {x | ((L.lhomWithConstantsMap ⇑eN).onFormula φ).Realize fun _ ↦ x}
+    change #rsN = κ
+    refine le_antisymm ((mk_subtype_le rsN).trans_eq hNcard) ?_
+    let φ' : F := ⟨φ, hφI⟩
+    rw [← mk_out κ]
+    /-
+    The constants indexed by `(φ', i)` give `κ` realizations by `T₂`, and `T₃` makes the resulting
+    map injective.
+    -/
+    have hφI' (i : I) : (L[[M]].con (φ', i) : N) ∈ rsN := by
+      simp [T₂] at hNT₂
+      simpa only [rsN, φ', Set.mem_ofPred_eq, subst, Sentence.Realize, Formula.Realize,
+        BoundedFormula.realize_subst, Term.realize_constants, LHom.onFormula,
+        LHom.realize_onBoundedFormula] using
+        hNT₂ (subst φ' i) φ' i rfl
+    let f : I → rsN := fun i ↦ ⟨(L[[M]].con (φ', i) : N), hφI' i⟩
+    refine Cardinal.mk_le_of_injective (f := f) ?_
+    intro i j hij
+    simp only [T₃] at hNT₃
+    have hNT₃' := (L[[M]].model_distinctConstantsTheory _).mp <| Theory.Model.mono hNT₃ <|
+      subset_iUnion_of_subset φ' fun ⦃a⦄ h ↦ h
+    simp only [Subtype.mk.injEq, f] at hij
+    exact congrArg Prod.snd <| hNT₃' (by simp) (by simp) hij
+  rw [← ((L.lhomWithConstantsMap ⇑eN).onFormula φ).finOneRealizationsEquiv.cardinal_eq]
+    at hφN
+  change #({x : Fin 1 → N | ψ.Realize (Sum.elim (eN ∘ b) x)}) = κ
+  convert hφN with v
+  simp only [(L.lhomWithConstantsMap ⇑eN).realize_onFormula, φ]
+  simp only [Formula.Realize, Formula.relabel, ← BoundedFormula.realize_constantsVarsEquiv,
+    _root_.Equiv.apply_symm_apply, BoundedFormula.realize_relabel, Nat.add_zero, Fin.castAdd_zero,
+    Fin.cast_refl, Function.comp_id, Fin.natAdd_zero]
+  congr!
+  ext (_ | _) <;> rfl
+
+/-- An infinite theory in a countable language has a definably full model of every infinite
+cardinality. -/
+theorem exists_model_of_card_definably_full
+    {κ : Cardinal.{w}} (hL : L.card ≤ ℵ₀)
+    (hT : ∃ M : ModelType.{u, v, max u v} T, Infinite M) (hκ : ℵ₀ ≤ κ) :
+    ∃ M : ModelType.{u, v, w} T, #M = κ ∧ L.DefinablyFull M := by
+  obtain ⟨M₀, hM₀card⟩ :=
+    Theory.exists_model_card_eq hT κ hκ
+      ((lift_le_aleph0.mpr hL).trans (aleph0_le_lift.mpr hκ))
+  let Stage := {M : ModelType.{u, v, w} T | #M = κ}
+  have hLκ : Cardinal.lift.{w} L.card ≤ Cardinal.lift.{max u v} κ :=
+    (lift_le_aleph0.mpr hL).trans (aleph0_le_lift.mpr hκ)
+  /- Apply the one-step construction to every model of cardinality `κ`. -/
+  have hsucc :
+      ∀ s : Stage, ∃ t : Stage, ∃ e : s.1 ↪ₑ[L] t.1,
+        ∀ {β : Type w} (ψ : L.Formula (β ⊕ Fin 1)) (b : β → s.1),
+          Set.Infinite {x : Fin 1 → s.1 | ψ.Realize (Sum.elim b x)} →
+            #({x : Fin 1 → t.1 | ψ.Realize (Sum.elim (e ∘ b) x)}) = κ := by
+    intro s
+    obtain ⟨N, e, hNcard, hfull⟩ :=
+      exists_elementaryExtension_card_eq_with_full_unary_realizations.{u, v, w, w}
+        T s.1 s.2 hκ hLκ
+    exact ⟨⟨N, hNcard⟩, e, hfull⟩
+  choose next nextEmb nextFull using hsucc
+  /-
+  Iterating the chosen extensions along `ℕ` produces an elementary chain in which every unary
+  formula over one stage is fully realized at the next stage.
+  -/
+  let stage : ℕ → Stage :=
+    fun n ↦ Nat.rec ⟨M₀, hM₀card⟩ (fun _ s ↦ next s) n
+  let M : ℕ → Type w := fun n ↦ (stage n).1
+  letI chainStruct : ∀ n, L.Structure (M n) :=
+    fun n ↦ (stage n).1.struc
+  let f : ∀ n, M n ↪ₑ[L] M (n + 1) := fun n ↦ by
+    simpa [M, stage, chainStruct] using nextEmb (stage n)
+  let C := ElementaryChain.ofNatSucc M f
+  haveI : Nonempty C.Limit := Nonempty.map (C.toLimit 0) M₀.instNonempty
+  haveI : C.Limit ⊨ T := C.limit_models T ⟨0, M₀.is_model⟩
+  /- The limit has cardinality `κ`, since all stages do and `κ` is infinite. -/
+  have hCκ : #C.Limit = κ := by
+    apply C.mk_limit_eq_of_forall_lift_mk_eq κ (le_of_eq_of_le rfl hκ)
+    intro i
+    cases i with
+    | zero => simpa [C, M, f, ElementaryChain.ofNatSucc, stage]
+    | succ n =>
+      simp only [lift_uzero]
+      exact (next (Nat.rec ⟨M₀, hM₀card⟩ (fun _ s ↦ next s) n)).2
+  refine ⟨ModelType.of T C.Limit, hCκ, ?_⟩
+  change L.DefinablyFull C.Limit
+  letI : Infinite C.Limit := infinite_iff.mpr <| hκ.trans_eq hCκ.symm
+  apply definablyFull_of_unary
+  unfold UnaryDefinablyFull
+  intro A X hAX hXI
+  /-
+  Replace the parameters defining `X` by a finite set, then move all of them into one common stage
+  of the chain.
+  -/
+  rw [Definable₁, definable_iff_finitely_definable] at hAX
+  rcases hAX with ⟨A₀, _, φ, hφ⟩
+  obtain ⟨i, v, hiv⟩ := C.exists_finite_common_stage fun a : A₀ ↦ a.1
+  let ψ : L.Formula (A₀ ⊕ Fin 1) := BoundedFormula.constantsVarsEquiv φ
+  /-
+  Elementarity transfers the infinitude of `X` back to the corresponding realization set at
+  stage `i`.
+  -/
+  have hψI : {x : Fin 1 → (stage i).1 | ψ.Realize (Sum.elim v x)}.Infinite := by
+    erw [← (C.toLimitElementary i).infinite_realizations_iff ψ v]
+    change {x : Fin 1 → C.Limit | ψ.Realize (Sum.elim (C.toLimit i ∘ v) x)}.Infinite
+    convert_to {x : Fin 1 → C.Limit | x 0 ∈ X}.Infinite using 1
+    · rw [hφ]
+      ext x
+      change ψ.Realize (Sum.elim (C.toLimit i ∘ v) x) ↔ φ.Realize x
+      simpa only [ψ, hiv] using!
+        BoundedFormula.realize_constantsVarsEquiv (φ := φ) (v := x)
+    · refine hXI.preimage (f := fun x : Fin 1 → C.Limit ↦ x 0) ?_
+      simp only [Fin.isValue, range_eval, subset_univ]
+  specialize nextFull (stage i) ψ v hψI
+  /-
+  The next stage contains `κ` realizations. Embedding them into the limit and identifying the
+  resulting realization set with `X` gives the required lower cardinal bound.
+  -/
+  apply le_antisymm (mk_set_le X)
+  let b : A₀ → C.Limit := C.toLimitElementary (i + 1) ∘ f i ∘ v
+  calc
+    #C.Limit = κ := hCκ
+    _ = _ := nextFull.symm
+    _ ≤ #↑{x : Fin 1 → C.Limit | ψ.Realize (Sum.elim b x)} := by
+      simpa [lift_id, b] using!
+        (C.toLimitElementary (i + 1)).mk_realizations_le ψ
+          (f i ∘ v)
+    _ = #{x : Fin 1 → C.Limit | x 0 ∈ X} := by
+      rw [hφ]
+      congr! with x
+      simp only [Formula.Realize, SetLike.coe_sort_coe, ← BoundedFormula.realize_constantsVarsEquiv,
+        ψ, b]
+      congr! with a
+      change C.toLimit (i + 1) (f i (v a)) = (a : C.Limit)
+      simpa [← congrFun hiv a, C] using! C.toLimit_map (Nat.le_succ i) (v a)
+    _ = _ :=
+      Cardinal.mk_congr <| (Equiv.funUnique (Fin 1) C.Limit).subtypeEquiv fun _ ↦ by simp
+
+end Theory
+
+end Language
+
+end FirstOrder
diff --git a/Mathlib/ModelTheory/Encoding.lean b/Mathlib/ModelTheory/Encoding.lean
index 1d91ab5a2079f7..d78b02178dc555 100644
--- a/Mathlib/ModelTheory/Encoding.lean
+++ b/Mathlib/ModelTheory/Encoding.lean
@@ -25,6 +25,10 @@ public import Mathlib.SetTheory.Cardinal.Arithmetic
 - `FirstOrder.Language.BoundedFormula.card_le` shows that the number of bounded formulas in
   `Σ n, L.BoundedFormula α n` is at most
   `max ℵ₀ (Cardinal.lift.{max u v} #α + Cardinal.lift.{u'} L.card)`.
+- `FirstOrder.Language.Formula.card_le` gives the same bound for `L.Formula α`.
+- `FirstOrder.Language.BoundedFormula.card_le_withConstants` and
+  `FirstOrder.Language.Formula.card_le_withConstants` make the contribution from parameters
+  explicit.
 
 ## TODO
 
@@ -298,6 +302,35 @@ theorem card_le : #(Σ n, L.BoundedFormula α n) ≤
   rw [← add_assoc, add_comm, ← add_assoc, ← add_assoc, aleph0_add_aleph0, add_assoc,
     add_eq_max le_rfl, add_assoc, card, Symbols, mk_sum, lift_add, lift_lift, lift_lift]
 
+theorem card_le_withConstants {β : Type w} : #(Σ n, L[[α]].BoundedFormula β n) ≤
+    max ℵ₀
+      (Cardinal.lift.{max (max u u') v} #β +
+        (Cardinal.lift.{max w u'} L.card + Cardinal.lift.{max (max u v) w} #α)) := by
+  simpa only [card_withConstants, lift_add, lift_lift] using
+    card_le (L := L[[α]]) (α := β)
+
+end BoundedFormula
+
+namespace Formula
+
+theorem card_le : #(L.Formula α) ≤
+    max ℵ₀ (Cardinal.lift.{max u v} #α + Cardinal.lift.{u'} L.card) :=
+  (Cardinal.mk_le_of_injective
+    (f := fun φ ↦ (⟨0, φ⟩ : Σ n, L.BoundedFormula α n)) sigma_mk_injective).trans
+      BoundedFormula.card_le
+
+theorem card_le_withConstants {β : Type w} : #(L[[α]].Formula β) ≤
+    max ℵ₀
+      (Cardinal.lift.{max (max u u') v} #β +
+        (Cardinal.lift.{max w u'} L.card + Cardinal.lift.{max (max u v) w} #α)) :=
+  (Cardinal.mk_le_of_injective
+    (f := fun φ ↦ (⟨0, φ⟩ : Σ n, L[[α]].BoundedFormula β n)) sigma_mk_injective).trans
+    BoundedFormula.card_le_withConstants
+
+end Formula
+
+namespace BoundedFormula
+
 section Countable
 
 variable [Countable α] [Countable L.Symbols]
diff --git a/Mathlib/ModelTheory/LanguageMap.lean b/Mathlib/ModelTheory/LanguageMap.lean
index b95a9c0830ea6f..df986c032be7b3 100644
--- a/Mathlib/ModelTheory/LanguageMap.lean
+++ b/Mathlib/ModelTheory/LanguageMap.lean
@@ -459,6 +459,33 @@ instance constantsOnSelfStructure : (constantsOn M).Structure M :=
 
 instance withConstantsSelfStructure : L[[M]].Structure M := inferInstance
 
+namespace LHom
+
+variable {L} {α : Type*} [L[[α]].Structure M] [(L.lhomWithConstants α).IsExpansionOn M]
+
+/-- A map between constant expansions is an expansion when it sends each new constant to its
+interpretation in the target structure. -/
+theorem lhomWithConstantsMap_isExpansionOn_of_eq
+    (f : α → M) (h : ∀ a : α, f a = ((L.con a : L[[α]].Constants) : M)) :
+    (L.lhomWithConstantsMap f).IsExpansionOn M := by
+  simp only [lhomWithConstantsMap]
+  constructor
+  · intro n g x
+    cases g with
+    | inl g => exact ((L.lhomWithConstants α).map_onFunction g x).symm
+    | inr g =>
+      cases n with
+      | zero =>
+        rw [Unique.eq_default x]
+        exact h g
+      | succ n => exact isEmptyElim g
+  · intro n R x
+    cases R with
+    | inl R => exact ((L.lhomWithConstants α).map_onRelation R x).symm
+    | inr R => exact isEmptyElim R
+
+end LHom
+
 instance withConstants_self_expansion : (lhomWithConstants L M).IsExpansionOn M :=
   ⟨fun _ _ => rfl, fun _ _ => rfl⟩
 

From 825f4f63cb5d7173f6a3b0316ad3ef747ae44e65 Mon Sep 17 00:00:00 2001
From: NoneMore <hellgoingup@outlook.com>
Date: Wed, 29 Jul 2026 01:43:08 +0800
Subject: [PATCH 11/11] update copyright information and author name

---
 Mathlib/ModelTheory/DefinablyFull.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/ModelTheory/DefinablyFull.lean b/Mathlib/ModelTheory/DefinablyFull.lean
index 9bb838d6d14f8c..cff8e18478b1d1 100644
--- a/Mathlib/ModelTheory/DefinablyFull.lean
+++ b/Mathlib/ModelTheory/DefinablyFull.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2026 NoneMore. All rights reserved.
+Copyright (c) 2026 Zikang Yu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: NoneMore
+Authors: Zikang Yu
 -/
 module