Highly order-transitive linear orders

The order-theoretic input of the countably-many-types project (issue #11, Marker Theorem 11.2): a linear order is highly order-transitive when every isomorphism between two finite increasing tuples extends to an order automorphism. Combined with the local EM equivariance package (Methods/LocalEMEquivariance.lean), such automorphisms of the skeleton induce structure automorphisms of the term model moving any increasing tuple of skeleton constants to any other, which is what collapses tuple types to finitely describable orbit data.

This file is the consumer-shaped INTERFACE: the definition and its transport/restriction lemmas. Existence at every infinite cardinality (Marker: the order of an ordered field) is a separate, deferred construction — the model-theoretic argument is developed conditionally on a highly order-transitive J.

def FirstOrder.HighlyOrderTransitive (J : Type u_1) [LinearOrder J] : Prop

A linear order is highly order-transitive when every isomorphism between two finite increasing tuples extends to an order automorphism: for all n and increasing n-tuples s, t, some e : J ≃o J has e (s i) = t i for all i.

Equations

• FirstOrder.HighlyOrderTransitive J = ∀ (n : ℕ) (s t : Fin n ↪o J), ∃ (e : J ≃o J), ∀ (i : Fin n), e (s i) = t i

theorem FirstOrder.HighlyOrderTransitive.of_orderIso {J : Type u_1} {J' : Type u_2} [LinearOrder J] [LinearOrder J'] (f : J ≃o J') (hJ : HighlyOrderTransitive J) : HighlyOrderTransitive J'

High order-transitivity transports along order isomorphisms.

theorem FirstOrder.HighlyOrderTransitive.exists_map_point {J : Type u_1} [LinearOrder J] (hJ : HighlyOrderTransitive J) (x y : J) : ∃ (e : J ≃o J), e x = y

The two-point instance consumed most often: any point moves to any other point.