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.

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 := ⋯ }