Internal Scott rank of structures with the self-extension property

If every finitely generated partial automorphism of a relational structure M extends to any given element, that is Language.IsExtensionPair M M, then two tuples of M with the same atomic type are back-and-forth equivalent at every level. Hence M stabilizes internally at zero, every tuple has orbit rank zero, and the internal Scott rank of M is one, the least possible value.

For countably generated structures the hypothesis is ultrahomogeneity (Mathlib's isUltrahomogeneous_iff_IsExtensionPair); it also holds for dense linear orders without endpoints of every cardinality. No countability is assumed.

theorem FirstOrder.Language.IsExtensionPair.selfStabilizesCompletely_zero {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] (h : L.IsExtensionPair M M) : TauCeti.SelfStabilizesCompletely M 0

A structure with the self-extension property stabilizes internally at zero.

theorem FirstOrder.Language.IsExtensionPair.selfStabilizationOrdinal_eq_zero {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] (h : L.IsExtensionPair M M) : TauCeti.selfStabilizationOrdinal M = 0

The least internal stabilization ordinal of a structure with the self-extension property is zero.

theorem FirstOrder.Language.IsExtensionPair.orbitRank_eq_zero {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] (h : L.IsExtensionPair M M) {n : ℕ} (a : Fin n → M) : TauCeti.orbitRank a = 0

Every finite tuple of a structure with the self-extension property has orbit rank zero.

theorem FirstOrder.Language.IsExtensionPair.internalScottRank_eq_one {L : Language} [L.IsRelational] {M : Type w} [L.Structure M] (h : L.IsExtensionPair M M) : TauCeti.internalScottRank M = 1

A structure with the self-extension property has internal Scott rank one.