Proof of CountableRefinementHypothesis

This file proves CountableRefinementHypothesis and provides unconditional wrappers for all Sentence.lean-level theorems. Together with the downstream wrappers in Rank.lean, Height.lean, CountableCorollary.lean, and CountingModels.lean, this recovers the full unconditional API.

Strategy

The proof uses the "constant chain" argument:

1. Self-stabilization (exists_complete_self_stabilization) gives α₀ < ω₁ where the internal BFEquiv relation on M is frozen.
2. Under self-stabilization, forth/back witnesses chosen at level α₀ automatically work at all higher levels (chain_step + witness_at_all_levels).
3. By transfinite induction (BFEquiv_of_all_finite_levels), BFEquiv (α₀+k) for all k upgrades to BFEquiv ε for all ε.
4. Hence no refinement ordinals exist above γ = sup_k(α₀+k) < ω₁, and R(n,a) ⊆ [0,γ) is countable.

Main Result

• countableRefinementHypothesis : CountableRefinementHypothesis L

Self-stabilization to full stabilization

The key insight: SelfStabilizesCompletely M α₀ (internal BFEquiv stabilization) implies that the back-and-forth game cannot create new refinements above α₀ + ω, because any forth/back witness at level α₀ already works at all higher levels (the "constant chain" argument). This avoids the need to count external BFEquiv types directly.

The Counting Lemma

theorem FirstOrder.Language.countableRefinementHypothesis {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] : L.CountableRefinementHypothesis

The countable refinement hypothesis holds for all countable relational languages.

For a countable structure M in a countable relational language, and any n-tuple a from M, the set of refinement ordinals R(n, a) = {ε < ω₁ | ∃ (N, b), BFEquiv ε ∧ ¬BFEquiv (succ ε)} is countable.

Proof: Self-stabilization (exists_complete_self_stabilization) gives α₀ < ω₁ where internal BFEquiv on M is frozen. For any ε above γ = sup_k(α₀+k) with BFEquiv ε n a b, the monotonicity of BFEquiv gives BFEquiv (α₀+k) for all k. The "constant chain" argument (witness_at_all_levels) shows that forth/back witnesses at level α₀ work at all higher levels (via self-stabilization + transitivity), so BFEquiv_of_all_finite_levels upgrades BFEquiv to the successor. Hence no refinement ordinals exist above γ < ω₁.

Unconditional Wrappers (Sentence.lean level)

Each theorem below is a one-liner applying countableRefinementHypothesis to the corresponding _of variant in Sentence.lean.

theorem FirstOrder.Language.exists_complete_stabilization {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] : ∃ α < Ordinal.omega 1, StabilizesCompletely M α

Complete stabilization below ω₁.

theorem FirstOrder.Language.scottSentence_characterizes {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (M : Type w) [L.Structure M] [Countable M] (N : Type w) [L.Structure N] [Countable N] : (scottSentence M).realizeAsSentence N ↔ Nonempty (L.Equiv M N)

The Scott sentence of M characterizes M up to isomorphism among countable structures.