A concrete assembled structure of internal Scott rank exactly ω

The elementary family: empty component language, default component ℕ, components B u := Fin (u + 1), allowed sets A n := {u | u ≤ n}. Every hypothesis of the conditional exact-rank theorem internalScottRank_eq_of_bounds is discharged, so the assembled structure has internal Scott rank exactly ω with no remaining component hypotheses (internalScottRank_exactOmega).

• No finite component is default-like (not_defaultLike), so (H_up) is vacuous.
• (H_sep) at position bound N uses level N + 2: a component at a position ≤ N is Fin (u + 1) with u ≤ N, and ℕ is equivalent to Fin (u + 1) at level k iff k ≤ u + 1 (bfEquiv_nat_fin_iff).
• (H_orb): every tuple of a pure set has orbit rank 0 (orbitRank_pure_eq_zero).
• AddNatClosed ω from the limit ω.
• Cofinal approximation at level k: the allowed row [0, 1, …, k] ends in k, whose component Fin (k + 1) is k-equivalent to ℕ and not isomorphic to it.

This establishes that the whole hypothesis package has a concrete instance. It does not supply an effective approximation family.

@[reducible, inline]

abbrev FirstOrder.Language.FiberAssembly.ExactOmega.Bfin : ℕ → Type

The components: Fin (u + 1).

Equations

• FirstOrder.Language.FiberAssembly.ExactOmega.Bfin u = Fin (u + 1)

def FirstOrder.Language.FiberAssembly.ExactOmega.Aiic : ℕ → Set ℕ

The allowed sets: at position n, the letters ≤ n.

Equations

• FirstOrder.Language.FiberAssembly.ExactOmega.Aiic n = Set.Iic n

@[reducible, inline]

abbrev FirstOrder.Language.FiberAssembly.ExactOmega.Carrier' : Type

The assembled structure.

Equations

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

theorem FirstOrder.Language.FiberAssembly.ExactOmega.nested : Nested Aiic

theorem FirstOrder.Language.FiberAssembly.ExactOmega.not_defaultLike (u : ℕ) : ¬DefaultLike Language.empty ℕ Bfin u

No finite component is isomorphic to the default ℕ.

theorem FirstOrder.Language.FiberAssembly.ExactOmega.upwardClosed : UpwardClosed (DefaultLike Language.empty ℕ Bfin)

theorem FirstOrder.Language.FiberAssembly.ExactOmega.sepBounded : SepBounded Language.empty ℕ Bfin Aiic Ordinal.omega0

(H_sep) at position bound N, with level N + 2.

theorem FirstOrder.Language.FiberAssembly.ExactOmega.orbitBounded : OrbitBounded Language.empty ℕ Bfin Aiic Ordinal.omega0

(H_orb): every fiber tuple has orbit rank 0 < ω.

theorem FirstOrder.Language.FiberAssembly.ExactOmega.addNatClosed : AddNatClosed Ordinal.omega0

def FirstOrder.Language.FiberAssembly.ExactOmega.rowRange (k : ℕ) : Row Aiic

The allowed row [0, 1, …, k].

Equations

• FirstOrder.Language.FiberAssembly.ExactOmega.rowRange k = ⟨List.range (k + 1), ⋯⟩

theorem FirstOrder.Language.FiberAssembly.ExactOmega.rowRange_ne (k : ℕ) : ↑(rowRange k) ≠ []

theorem FirstOrder.Language.FiberAssembly.ExactOmega.rowRange_getLast (k : ℕ) : (↑(rowRange k)).getLast ⋯ = k

theorem FirstOrder.Language.FiberAssembly.ExactOmega.cofinalApprox : CofinalApprox Language.empty ℕ Bfin Aiic Ordinal.omega0

Cofinal approximation: at level k, the row [0, …, k].

theorem FirstOrder.Language.FiberAssembly.ExactOmega.internalScottRank_exactOmega : internalScottRank Carrier' = Ordinal.omega0

The assembled structure has internal Scott rank exactly ω.