Tail-indiscernibility: the eventually-form EM adapter

The EM stretching pipeline consumes source-side indiscernibility in exactly one place: the finite-satisfiability lemma interprets the finitely many constants of a finite piece of the template theory by a freely chosen strictly monotone tuple of the source sequence, and collapses template truth to realization at that tuple. Consequently full indiscernibility (all tuples agree) is more than is needed: it suffices that for each formula of the family there is a cutoff beyond which all strictly monotone tuples agree — tail indiscernibility — because the interpreting tuple may simply be chosen beyond the maximum cutoff of the finitely many formulas involved.

This matters for Morley–Hanf: the classical Erdős–Rado extraction from a model of size ≥ ℶ_ω₁ produces (per arity, after finitely many partition steps) exactly tail indiscernibility of an ℕ-indexed sequence, while full simultaneous indiscernibility across all arities is not what the classical argument yields in the source model. This file weakens the EM interface accordingly:

• IsLomega1omegaIndiscernibleOnTail a Γ — per-formula cutoffs beyond which strictly monotone tuples agree (ℕ-indexed sequences);
• tailTemplateOfSeq a — the eventually-form template: a formula is true if all sufficiently deep strictly monotone tuples realize it;
• tailTemplateOfSeq_truth_iff — the truth collapse at any tuple beyond a cutoff;
• IsLomega1omegaIndiscernibleOnTail.templateTheoryOn_finitelySatisfiable — the deep-tuple finite-satisfiability lemma (mirroring the full-indiscernibility proof, with the interpreting embedding placed beyond the joint cutoff);
• …templateTheoryOfSeq_isFinitelySatisfiable and …templateTheoryOfSeq_model_of_compact — finite satisfiability of the tail-template theory, and the one application of a Theoryω.OrdinaryCompactness oracle that turns it into a model;
• …stretch_restricted_of_model and …stretch_restricted_sequence_of_model — stretching from that model, the honest residual which assumes no compactness at all.

The downstream consumer is hasArbLargeModels_of_tail_extraction in InfinitaryLogic/Conditional/MorleyHanfTransfer.lean.

Tail indiscernibility and the eventually-form template

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.isLomega1omegaIndiscernibleOnTail {L : Language} {M : Type u_1} [L.Structure M] {a : ℕ → M} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (h : IsLomega1omegaIndiscernibleOn a Γ) : IsLomega1omegaIndiscernibleOnTail a Γ

Full restricted indiscernibility gives tail indiscernibility (cutoff 0).

theorem FirstOrder.Language.exists_strictMono_of_le (n N : ℕ) : ∃ (s : Fin n → ℕ), StrictMono s ∧ ∀ (k : Fin n), N ≤ s k

Strictly monotone tuples exist above any cutoff.

def FirstOrder.Language.tailTemplateOfSeq {L : Language} {M : Type u_1} [L.Structure M] (a : ℕ → M) : L.Lomega1omegaTemplate

The eventually-form template of a sequence: a formula is true if all sufficiently deep strictly monotone tuples realize it. For a tail-indiscernible sequence this is well-defined in the sense of tailTemplateOfSeq_truth_iff.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOnTail.tailTemplateOfSeq_truth_iff {L : Language} {M : Type u_1} [L.Structure M] {a : ℕ → M} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (h : IsLomega1omegaIndiscernibleOnTail a Γ) {n : ℕ} {φ : L.BoundedFormulaω Empty n} (hφ : ⟨n, φ⟩ ∈ Γ) : ∃ (N : ℕ), ∀ (s : Fin n → ℕ), StrictMono s → (∀ (k : Fin n), N ≤ s k) → ((tailTemplateOfSeq a).truth φ ↔ φ.Realize Empty.elim (a ∘ s))

Truth collapse for the tail template: beyond a suitable cutoff, the template's value at a formula of the family equals the truth value at any strictly monotone tuple.

Deep-tuple finite satisfiability

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOnTail.templateTheoryOn_finitelySatisfiable {L : Language} {M : Type u_1} [L.Structure M] {a : ℕ → M} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (h : IsLomega1omegaIndiscernibleOnTail a Γ) {J : Type u} [LinearOrder J] {F : Set (L.withConstants J).Sentenceω} (hFin : F.Finite) (hSub : F ⊆ (tailTemplateOfSeq a).templateTheoryOn Γ J) : ∃ (σ : J → M), ∀ τ ∈ F, τ.Realize M

Finite satisfiability in the source model from tail indiscernibility: every finite subset of the tail-template theory is satisfiable in the source model. Mirrors IsLomega1omegaIndiscernibleOn.templateTheoryOn_finitelySatisfiable, with the interpreting order embedding placed beyond the joint cutoff of the finitely many formulas involved.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOnTail.templateTheoryOfSeq_finitelySatisfiable {L : Language} {M : Type u_1} [L.Structure M] {a : ℕ → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (h : IsLomega1omegaIndiscernibleOnTail a (Set.range s)) {J : Type u} [LinearOrder J] {F : Set (L.withConstants J).Sentenceω} (hFin : F.Finite) (hSub : F ⊆ (tailTemplateOfSeq a).templateTheoryOfSeq s J) : ∃ (σ : J → M), ∀ τ ∈ F, τ.Realize M

Sequence-indexed wrapper.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOnTail.templateTheoryOfSeq_isFinitelySatisfiable {L : Language} {M : Type} [L.Structure M] {a : ℕ → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (h : IsLomega1omegaIndiscernibleOnTail a (Set.range s)) {J : Type u} [LinearOrder J] : Theoryω.IsFinitelySatisfiable ((tailTemplateOfSeq a).templateTheoryOfSeq s J)

Finite satisfiability of the tail-template theory, as the named property.

The Nonempty component of Theoryω.IsSatisfiable is supplied by the source sequence itself: a : ℕ → M inhabits M. No extra hypothesis is needed, and none should be added — a template built from an indiscernible sequence always has a witness.

Compact-oracle stretching from tail indiscernibility

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOnTail.templateTheoryOfSeq_model_of_compact {L : Language} {M : Type} [L.Structure M] {a : ℕ → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (h : IsLomega1omegaIndiscernibleOnTail a (Set.range s)) {J : Type u} [LinearOrder J] (hCompact : Theoryω.OrdinaryCompactness (L.withConstants J)) : Theoryω.IsSatisfiable ((tailTemplateOfSeq a).templateTheoryOfSeq s J)

Compact-oracle adapter under tail indiscernibility.

Stretching from a model of the tail-template theory (honest residual)

The compact-oracle lemmas above assume full L_{ω₁ω} compactness for L[[J]] (false in general). But the pipeline only ever needs that the specific tail-template theory — which is finitely satisfiable by templateTheoryOn_finitelySatisfiable — has some model. The lemmas below take exactly that model as input; the broad compactness oracle factors through them.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOnTail.stretch_restricted_of_model {L : Language} {M : Type} [L.Structure M] {a : ℕ → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) {J : Type u} [LinearOrder J] (hModel : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model ((tailTemplateOfSeq a).templateTheoryOfSeq s J) N) : ∃ (N : Type) (x : (L.withConstants J).Structure N), ∀ (i : ℕ) (t : Fin (s i).fst ↪o J), (Lomega1omegaTemplate.templateSentence (s i).snd t).Realize N ↔ (tailTemplateOfSeq a).truth (s i).snd

EM stretching (sentence form) from a model of the tail-template theory. Needs only that the (proved finitely-satisfiable) tail-template theory over J has a model — not a compactness oracle.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOnTail.stretch_restricted_sequence_of_model {L : Language} {M : Type} [L.Structure M] {a : ℕ → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) {J : Type u} [LinearOrder J] (hModel : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model ((tailTemplateOfSeq a).templateTheoryOfSeq s J) N) : ∃ (N : Type) (x : (L.withConstants J).Structure N) (b : J → N), ∀ (i : ℕ) (t : Fin (s i).fst ↪o J), (s i).snd.Realize Empty.elim (b ∘ ⇑t) ↔ (tailTemplateOfSeq a).truth (s i).snd

EM stretching (sequence form) from a model of the tail-template theory.