The compact ordinal space and coordinate projections

@[reducible, inline]

abbrev OrderClosures.GaoIndex (ξ : Ordinal.{u}) : Set Ordinal.{u}

Coordinate indices in the compact ordinal construction.

Equations

• OrderClosures.GaoIndex ξ = Set.Iic (Ordinal.omega0 ^ ξ + 1)

def OrderClosures.GaoCompactSpace (ξ : Ordinal.{u}) : Set (↑(GaoIndex ξ) → Bool)

The closed subspace of the Cantor cube used in the proof of thm:solid-iterations.

Equations

• OrderClosures.GaoCompactSpace ξ = {x : ↑(OrderClosures.GaoIndex ξ) → Bool | ∀ (a b : ↑(OrderClosures.GaoIndex ξ)), OrderClosures.cnfExtensionLT ↑a ↑b → x a ≤ x b}

noncomputable def OrderClosures.ordinalProjection (ξ : Ordinal.{u}) (ζ : ↑(GaoIndex ξ)) : C(↑(GaoCompactSpace ξ), ℝ)

Coordinate projection π_ζ on the Gao compact space.

Equations

• OrderClosures.ordinalProjection ξ ζ = { toFun := fun (x : ↑(OrderClosures.GaoCompactSpace ξ)) => if ↑x ζ = true then 1 else 0, continuous_toFun := ⋯ }

theorem OrderClosures.continuousMap_exists_finite_coordinates {I : Type u} {K : Set (I → Bool)} (f : C(↑K, ℝ)) (x : ↑K) {V : Set ℝ} (hV : IsOpen V) (hxV : f x ∈ V) : ∃ (F : Finset I), ∀ (y : ↑K), (∀ i ∈ F, ↑y i = ↑x i) → f y ∈ V

Extracts finitely many Cantor-cube coordinates controlling a continuous real map; used to prove the incomparable-projection infimum formula.

noncomputable def OrderClosures.leastCNFExponent (ζ : Ordinal.{u}) : Ordinal.{u}

The least exponent in the Cantor normal form of an ordinal (zero at the empty normal form).

Equations

• OrderClosures.leastCNFExponent ζ = (Option.map Prod.fst (Ordinal.CNF Ordinal.omega0 ζ).getLast?).getD 0

def OrderClosures.GaoStageIndices (ξ β : Ordinal.{u}) : Set ↑(GaoIndex ξ)

The index set Z_β from Claim 3.

Equations

• OrderClosures.GaoStageIndices ξ β = {ζ : ↑(OrderClosures.GaoIndex ξ) | ↑ζ ≤ Ordinal.omega0 ^ ξ ∧ OrderClosures.leastCNFExponent ↑ζ < β}

def OrderClosures.GaoStageSet (ξ β : Ordinal.{u}) : Set C(↑(GaoCompactSpace ξ), ℝ)

The solid set S_β from Claim 3.

Equations

• OrderClosures.GaoStageSet ξ β = {f : C(↑(OrderClosures.GaoCompactSpace ξ), ℝ) | ∃ ζ ∈ OrderClosures.GaoStageIndices ξ β, |f| ≤ OrderClosures.ordinalProjection ξ ζ}

theorem OrderClosures.isSolid_gaoStageSet (ξ β : Ordinal.{u}) : LatticeOrderedAddCommGroup.IsSolid (GaoStageSet ξ β)

Records solidity of each Gao stage set; used to invoke the solid form of order adherence in the stage formula.

theorem OrderClosures.ordinalProjection_incomparable_iInf (ξ : Ordinal.{u}) (Z : Set ↑(GaoIndex ξ)) (hZ : Z.Infinite) (hinc : Z.Pairwise fun (ζ ζ' : ↑(GaoIndex ξ)) => ¬cnfExtensionLE ↑ζ ↑ζ') : IsGLB (ordinalProjection ξ '' Z) 0

Claim 1 in the proof of Theorem thm:solid-iterations.

theorem OrderClosures.ordinalProjection_le_iff (ξ : Ordinal.{u}) (a b : ↑(GaoIndex ξ)) : ordinalProjection ξ a ≤ ordinalProjection ξ b ↔ cnfExtensionLE ↑a ↑b

Characterizes order between coordinate projections by CNF extension; used in all dominator and strict-stage arguments.

noncomputable def OrderClosures.leadingCNFTerm (a : Ordinal.{u}) : Ordinal.{u}

The leading monomial of an ordinal's canonical normal form; isolated for the singleton-chain supremum analysis.

Equations

• OrderClosures.leadingCNFTerm a = Ordinal.omega0 ^ Ordinal.log Ordinal.omega0 a * (a / Ordinal.omega0 ^ Ordinal.log Ordinal.omega0 a)

theorem OrderClosures.cnf_singleton_le_leadingCNFTerm {q a γ d : Ordinal.{u}} (hq : Ordinal.CNF Ordinal.omega0 q = [(γ, d)]) (hqa : q ≤ a) : q ≤ leadingCNFTerm a

Bounds a singleton CNF monomial by the leading term of an ordinal; used to identify possible upper bounds of singleton chains.

theorem OrderClosures.cnf_singleton_spec {q γ d : Ordinal.{u}} (hq : Ordinal.CNF Ordinal.omega0 q = [(γ, d)]) : q = Ordinal.omega0 ^ γ * d ∧ 0 < d ∧ d < Ordinal.omega0 ∧ Ordinal.log Ordinal.omega0 q = γ

Gives the canonical CNF description of a singleton omega monomial; used to translate singleton-chain inequalities into exponent inequalities.

theorem OrderClosures.cnf_eq_singleton_of_isLUB (Q : Set Ordinal.{u}) (a : Ordinal.{u}) (hQ : Q.Nonempty) (hsingle : ∀ q ∈ Q, ∃ (γ : Ordinal.{u}) (d : Ordinal.{u}), Ordinal.CNF Ordinal.omega0 q = [(γ, d)]) (hlub : IsLUB Q a) : ∃ (γ : Ordinal.{u}) (d : Ordinal.{u}), Ordinal.CNF Ordinal.omega0 a = [(γ, d)]

Shows that the least upper bound of a nonempty singleton-monomial chain is itself a singleton monomial; used in the chain-supremum analysis.

theorem OrderClosures.cnf_singleton_exponent_lt_of_isLUB_not_mem (Q : Set Ordinal.{u}) (a : Ordinal.{u}) (hsingle : ∀ q ∈ Q, ∃ (γ : Ordinal.{u}) (d : Ordinal.{u}), Ordinal.CNF Ordinal.omega0 q = [(γ, d)]) (hlub : IsLUB Q a) (haQ : a ∉ Q) {q β c γ d : Ordinal.{u}} (hqQ : q ∈ Q) (hq : Ordinal.CNF Ordinal.omega0 q = [(β, c)]) (ha : Ordinal.CNF Ordinal.omega0 a = [(γ, d)]) : β < γ

Makes the exponent of a nonattained singleton-chain supremum strictly larger than every member exponent; used at the limit case of the CNF chain.

theorem OrderClosures.CNFListLT.eq_dropLast_of_length_eq {l m : List (Ordinal.{u} × Ordinal.{u})} (h : CNFListLT l m) (hlen : m.length = l.length) : ∃ (x : Ordinal.{u} × Ordinal.{u}) (y : Ordinal.{u} × Ordinal.{u}), l = l.dropLast ++ [x] ∧ m = l.dropLast ++ [y] ∧ CNFStep l.dropLast x y

Identifies an equal-length CNF extension as deletion of the last source term; used to analyze stabilization in chains of extensions.

theorem OrderClosures.cnfExtensionLE_chain_lub (ξ : Ordinal.{u}) (Z : Set ↑(GaoIndex ξ)) (α : ↑(GaoIndex ξ)) (hchain : ∀ ⦃ζ : ↑(GaoIndex ξ)⦄, ζ ∈ Z → ∀ ⦃ζ' : ↑(GaoIndex ξ)⦄, ζ' ∈ Z → cnfExtensionLE ↑ζ ↑ζ' ∨ cnfExtensionLE ↑ζ' ↑ζ) (hsup : IsLUB ((fun (ζ : ↑(GaoIndex ξ)) => ↑ζ) '' Z) ↑α) (ζ : ↑(GaoIndex ξ)) : ζ ∈ Z → cnfExtensionLE ↑ζ ↑α

Proves that the ordinary supremum of a nonempty extension chain remains above every member in cnfExtensionLE; used by ordinalProjection_chain_iSup.

theorem OrderClosures.leastCNFExponent_chain_lub_le (ξ γ : Ordinal.{u}) (Z : Set ↑(GaoIndex ξ)) (α : ↑(GaoIndex ξ)) (hne : Z.Nonempty) (hchain : ∀ ⦃ζ : ↑(GaoIndex ξ)⦄, ζ ∈ Z → ∀ ⦃ζ' : ↑(GaoIndex ξ)⦄, ζ' ∈ Z → cnfExtensionLE ↑ζ ↑ζ' ∨ cnfExtensionLE ↑ζ' ↑ζ) (hsup : IsLUB ((fun (ζ : ↑(GaoIndex ξ)) => ↑ζ) '' Z) ↑α) (hleast : ∀ ζ ∈ Z, leastCNFExponent ↑ζ < γ) : leastCNFExponent ↑α ≤ γ

Controls the least CNF exponent of a chain supremum; used to keep the supremum projection inside the required Gao stage.

theorem OrderClosures.ordinalProjection_chain_iSup (ξ : Ordinal.{u}) (Z : Set ↑(GaoIndex ξ)) (α : ↑(GaoIndex ξ)) (hne : Z.Nonempty) (hchain : ∀ ⦃ζ : ↑(GaoIndex ξ)⦄, ζ ∈ Z → ∀ ⦃ζ' : ↑(GaoIndex ξ)⦄, ζ' ∈ Z → cnfExtensionLE ↑ζ ↑ζ' ∨ cnfExtensionLE ↑ζ' ↑ζ) (hsup : IsLUB ((fun (ζ : ↑(GaoIndex ξ)) => ↑ζ) '' Z) ↑α) : IsLUB (ordinalProjection ξ '' Z) (ordinalProjection ξ α)

Claim 2 in the proof of Theorem thm:solid-iterations.