Highly order-transitive orders of every infinite cardinality (issue #11 unit 6b)

For every infinite cardinal κ there is a highly order-transitive linear order of cardinality exactly κ — bundled as HighlyTransitiveOrderAt κ (avoiding awkward existential typeclass binders), with the existential corollary exported.

The construction is a Hahn-series generated subfield: over an index type X of cardinality κ, take the lexicographic value group Γ = Lex (X →₀ ℤ) and the lexicographically ordered Hahn-series field K = Lex ℚ⟦Γ⟧, embed X by distinct monomials x ↦ single (single x 1) 1, and let J be the subfield they generate. The monomial map is injective, so Subfield.cardinalMk_closure gives #J = #X = κ; J inherits a linear ordered field structure, and unit 6a (HighlyOrderTransitive.of_field) makes it highly order-transitive.

Implementation note: Mathlib.RingTheory.HahnSeries.Summable must be imported explicitly — the lexicographic Hahn import alone does not load the field instance.

structure FirstOrder.HighlyTransitiveOrderAt (κ : Cardinal.{0}) : Type 1

A bundled highly order-transitive linear order of prescribed cardinality.

• Carrier : Type

  The carrier.

• linearOrder : LinearOrder self.Carrier

  The order.

• card_eq : Cardinal.mk self.Carrier = κ

  The carrier has size exactly κ.

• highlyTransitive : HighlyOrderTransitive self.Carrier

  High order-transitivity.

@[reducible, inline]

abbrev FirstOrder.hahnGamma (X : Type) : Type

The lexicographic value group of the construction.

Equations

• FirstOrder.hahnGamma X = Lex (X →₀ ℤ)

@[reducible, inline]

abbrev FirstOrder.hahnField (X : Type) [LinearOrder X] : Type

The ambient lexicographically ordered Hahn-series field.

Equations

• FirstOrder.hahnField X = Lex (HahnSeries (FirstOrder.hahnGamma X) ℚ)

noncomputable def FirstOrder.hahnMonomial (X : Type) [LinearOrder X] (x : X) : hahnField X

The monomial embedding of the index type.

Equations

• FirstOrder.hahnMonomial X x = toLex ((HahnSeries.single (toLex (Finsupp.single x 1))) 1)

theorem FirstOrder.hahnMonomial_injective (X : Type) [LinearOrder X] : Function.Injective (hahnMonomial X)

noncomputable def FirstOrder.hahnSubfield (X : Type) [LinearOrder X] : Subfield (hahnField X)

The generated subfield: the ordered field of cardinality #X.

Equations

• FirstOrder.hahnSubfield X = Subfield.closure (Set.range (FirstOrder.hahnMonomial X))

theorem FirstOrder.mk_hahnSubfield (X : Type) [LinearOrder X] [Infinite X] : Cardinal.mk ↥(hahnSubfield X) = Cardinal.mk X

noncomputable def FirstOrder.highlyTransitiveOrderAt (κ : Cardinal.{0}) (hκ : Cardinal.aleph0 ≤ κ) : HighlyTransitiveOrderAt κ

Highly order-transitive orders exist at every infinite cardinality (bundled form).

Equations

• FirstOrder.highlyTransitiveOrderAt κ hκ = { Carrier := ↥(FirstOrder.hahnSubfield κ.ord.ToType), linearOrder := inferInstance, card_eq := ⋯, highlyTransitive := ⋯ }

theorem FirstOrder.exists_highlyTransitive_linearOrder (κ : Cardinal.{0}) (hκ : Cardinal.aleph0 ≤ κ) : ∃ (J : Type) (x : LinearOrder J), Cardinal.mk J = κ ∧ HighlyOrderTransitive J

The existential corollary — the acceptance signature of issue #11 unit 6.