Extraction Scaffolding for Indiscernible Sequences

This file provides the model-theoretic scaffolding that reduces the task "extract a pairwise-distinct ℕ-indexed restricted-indiscernible sequence from a large model" (MorleyHanfExtraction) to a smaller combinatorial- model-theoretic residual (a per-formula partition step).

Main definitions

• IsIndiscernibleOnSet a Γ S : a : I → M is indiscernible on the subset S : Set I for the family of formulas Γ. Equivalently, for every ⟨n, φ⟩ ∈ Γ and every two strictly-increasing tuples t, t' : Fin n → I with all entries in S, the truth values of φ on a ∘ t and a ∘ t' agree.

Main results

• IsIndiscernibleOnSet.toLomega1omegaIndiscernibleOn (sequence-level reduction): if f : ℕ → I is strictly monotone and Set.range f is IsIndiscernibleOnSet for the range of a formula sequence s, then the assembled a ∘ f : ℕ → M is IsLomega1omegaIndiscernibleOn (Set.range s).

Scope

This file does NOT prove any combinatorial extraction theorem — the goal is to provide the model-theoretic bridge that turns an already-extracted indiscernible subset into the restricted-indiscernible sequence consumed by the Phase-2 bridge hasArbLargeModels_of_restricted_extraction. The existence of the indiscernible subset (Erdős–Rado-style partition content) remains a separate hypothesis for a future tranche.

Indiscernibility on a subset

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

IsIndiscernibleOnSet a Γ S expresses that a : I → M is indiscernible on the subset S ⊆ I for the family of formulas Γ ⊆ Σ n, L.BoundedFormulaω Empty n: for every ⟨n, φ⟩ ∈ Γ and every two strictly-increasing n-tuples drawn from S, the truth values of φ on the corresponding a-tuples agree.

This is the natural "homogeneous subset" notion used in Erdős–Rado-style extraction arguments: a set S is IsIndiscernibleOnSet for Γ iff all Γ-formulas have constant truth on strictly-increasing tuples in S.

Equations

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

theorem FirstOrder.Language.IsIndiscernibleOnSet.mono {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] {a : I → M} {Γ Γ' : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (hΓ : Γ ⊆ Γ') {S S' : Set I} (hS : S ⊆ S') (h : IsIndiscernibleOnSet a Γ' S') : IsIndiscernibleOnSet a Γ S

Monotonicity: shrinking either the formula family or the subset preserves indiscernibility.

Sequence-level reduction to IsLomega1omegaIndiscernibleOn

theorem FirstOrder.Language.IsIndiscernibleOnSet.toLomega1omegaIndiscernibleOn {L : Language} {I : Type w} [LinearOrder I] {M : Type u_1} [L.Structure M] (a : I → M) (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (f : ℕ → I) (hf : StrictMono f) (hInd : IsIndiscernibleOnSet a (Set.range s) (Set.range f)) : IsLomega1omegaIndiscernibleOn (a ∘ f) (Set.range s)

Sequence-level reduction: if f : ℕ → I is strictly monotone and its range is IsIndiscernibleOnSet for the range of a formula sequence s, then the composed sequence a ∘ f : ℕ → M is IsLomega1omegaIndiscernibleOn (Set.range s).

This is the bridge from "extracted indiscernible subset" to "restricted- indiscernible ℕ-sequence" consumed by MorleyHanfExtraction.