Tail-restricted L_{ω₁ω} indiscernibility (neutral definition)

The bare definition of tail-restricted indiscernibility, factored out so both the EM stretching pipeline (Methods/EM/TailAdapter.lean, which keeps every EM-dependent downstream lemma) and the deliberately EM-free local EMContext re-base (Methods/LocalEMContext.lean) can refer to it without either importing the other.

The definition depends only on BoundedFormulaω.Realize, StrictMono, and ℕ/Fin — nothing from the EM/Admissible stack — so this file sits low in the import graph. It is on the default surface (imported by TailAdapter.lean → Admissible.lean); being neutral and tiny, that is harmless, unlike routing the def through the WIP-excluded LocalEMSupport.lean.

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

Tail-restricted indiscernibility: for every formula of the family there is a cutoff beyond which all strictly monotone tuples of the sequence agree. Weaker than IsLomega1omegaIndiscernibleOn (which is the cutoff-0 case), and the form actually produced by Erdős–Rado extraction arguments.

Equations

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