Adherence formulas for Gao stages

def OrderClosures.gaoDominators (ξ γ : Ordinal.{u}) (b : C(↑(GaoCompactSpace ξ), ℝ)) : Set ↑(GaoIndex ξ)

Stage indices whose coordinate projections dominate a given function; used to select finite minimal dominators.

Equations

• OrderClosures.gaoDominators ξ γ b = {ζ : ↑(OrderClosures.GaoIndex ξ) | ζ ∈ OrderClosures.GaoStageIndices ξ γ ∧ b ≤ OrderClosures.ordinalProjection ξ ζ}

def OrderClosures.gaoMinimalDominators (ξ γ : Ordinal.{u}) (b : C(↑(GaoCompactSpace ξ), ℝ)) : Set ↑(GaoIndex ξ)

Minimal elements of the dominator set in the CNF extension order; used to reduce a positive directed family to finitely many coordinates.

Equations

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

theorem OrderClosures.gaoDominators_nonempty (ξ γ : Ordinal.{u}) {b : C(↑(GaoCompactSpace ξ), ℝ)} (hb0 : 0 ≤ b) (hb : b ∈ GaoStageSet ξ γ) : (gaoDominators ξ γ b).Nonempty

Extracts a coordinate projection dominating a positive Gao-stage element; this starts the finite-minimal-dominator reduction.

theorem OrderClosures.gaoDominator_above_minimal (ξ γ : Ordinal.{u}) {b : C(↑(GaoCompactSpace ξ), ℝ)} {ζ : ↑(GaoIndex ξ)} (hζ : ζ ∈ gaoDominators ξ γ b) : ∃ μ ∈ gaoMinimalDominators ξ γ b, cnfExtensionLE ↑μ ↑ζ

Refines any dominator to a minimal one; used to replace arbitrary dominating coordinates by a finite canonical family.

theorem OrderClosures.gaoMinimalDominators_pairwise (ξ γ : Ordinal.{u}) (b : C(↑(GaoCompactSpace ξ), ℝ)) : (gaoMinimalDominators ξ γ b).Pairwise fun (μ ν : ↑(GaoIndex ξ)) => ¬cnfExtensionLE ↑μ ↑ν

Shows that distinct minimal dominators are CNF-incomparable; used with the incomparable-projection infimum theorem.

theorem OrderClosures.gaoMinimalDominators_finite (ξ γ : Ordinal.{u}) {b : C(↑(GaoCompactSpace ξ), ℝ)} (hb0 : 0 ≤ b) (hbne : b ≠ 0) : (gaoMinimalDominators ξ γ b).Finite

Proves finiteness of the minimal dominator family; needed to combine it with directedness of the positive approximating set.

theorem OrderClosures.directedPositive_gaoStage_dominated (ξ γ : Ordinal.{u}) {z : C(↑(GaoCompactSpace ξ), ℝ)} (hz : z ∈ directedPositiveAdherence (GaoStageSet ξ γ)) : ∃ (α : ↑(GaoIndex ξ)), ↑α ≤ Ordinal.omega0 ^ ξ ∧ leastCNFExponent ↑α ≤ γ ∧ z ≤ ordinalProjection ξ α

Produces one Gao-stage coordinate dominating an entire directed positive family; this is the main input to the forward adherence inclusion.

theorem OrderClosures.orderAdherence_gaoStage_subset (ξ γ : Ordinal.{u}) : orderAdherence (GaoStageSet ξ γ) ⊆ GaoStageSet ξ (γ + 1)

Establishes the forward inclusion for one order-adherence step by using a single coordinate dominator.

def OrderClosures.singletonCNFBelow (γ : Ordinal.{u}) : Set Ordinal.{u}

Singleton omega monomials with exponent below γ; used as the directed approximating family for a limit-stage coordinate.

Equations

• OrderClosures.singletonCNFBelow γ = {q : Ordinal.{?u.1} | ∃ (δ : Ordinal.{?u.1}) (d : Ordinal.{?u.1}), Ordinal.CNF Ordinal.omega0 q = [(δ, d)] ∧ q < Ordinal.omega0 ^ γ}

theorem OrderClosures.singletonCNFBelow_isLUB (γ : Ordinal.{u}) (hγ : γ ≠ 0) : IsLUB (singletonCNFBelow γ) (Ordinal.omega0 ^ γ)

Shows that singleton CNF monomials below γ have supremum ω^γ; used to construct the reverse adherence approximation at limit exponents.

theorem OrderClosures.singletonCNF_step_of_lt {q r δ d ε e : Ordinal.{u}} (hq : Ordinal.CNF Ordinal.omega0 q = [(δ, d)]) (hr : Ordinal.CNF Ordinal.omega0 r = [(ε, e)]) (hqr : q < r) : ε = δ ∧ d < e ∨ δ < ε

Turns a strict exponent inequality into a strict CNF extension of singleton monomials; used by gaoIndex_approximation.

theorem OrderClosures.cnfValue_add_singleton_below (pre : List (Ordinal.{u} × Ordinal.{u})) (γ : Ordinal.{u}) (n : ℕ) (hpreSorted : List.Pairwise (fun (x y : Ordinal.{u}) => y < x) (List.map Prod.fst pre)) (hpreAbove : ∀ x ∈ pre, γ < x.1) (hprePos : ∀ x ∈ pre, 0 < x.2) (hpreLt : ∀ x ∈ pre, x.2 < Ordinal.omega0) (q : Ordinal.{u}) (hq : q ∈ singletonCNFBelow γ) : ∃ (δ : Ordinal.{u}) (d : Ordinal.{u}), Ordinal.CNF Ordinal.omega0 q = [(δ, d)] ∧ δ < γ ∧ Ordinal.CNF Ordinal.omega0 (cnfValue pre + Ordinal.omega0 ^ γ * ↑n + q) = if n = 0 then pre ++ [(δ, d)] else pre ++ [(γ, ↑n), (δ, d)]

Appending a smaller singleton CNF term to a finite prefix computes its normal form.

theorem OrderClosures.gaoIndex_approximation (ξ γ : Ordinal.{u}) (hγ : γ ≠ 0) (ζ : ↑(GaoIndex ξ)) (hζbound : ↑ζ ≤ Ordinal.omega0 ^ ξ) (hζleast : leastCNFExponent ↑ζ = γ) : ∃ (Z : Set ↑(GaoIndex ξ)), Z.Nonempty ∧ (∀ η ∈ Z, η ∈ GaoStageIndices ξ γ) ∧ (∀ ⦃η : ↑(GaoIndex ξ)⦄, η ∈ Z → ∀ ⦃η' : ↑(GaoIndex ξ)⦄, η' ∈ Z → cnfExtensionLE ↑η ↑η' ∨ cnfExtensionLE ↑η' ↑η) ∧ IsLUB ((fun (η : ↑(GaoIndex ξ)) => ↑η) '' Z) ↑ζ

Builds a directed family of earlier-stage indices whose projections order converge to a prescribed next-stage projection.

theorem OrderClosures.gaoStage_succ_subset_orderAdherence (ξ γ : Ordinal.{u}) (hγ : γ ≠ 0) : GaoStageSet ξ (γ + 1) ⊆ orderAdherence (GaoStageSet ξ γ)

Establishes the reverse inclusion for a successor Gao stage from the explicit coordinate approximations.

theorem OrderClosures.orderAdherence_gaoStage (ξ γ : Ordinal.{u}) (hγ : γ ≠ 0) : orderAdherence (GaoStageSet ξ γ) = GaoStageSet ξ (γ + 1)

Packages both inclusions into the one-step Gao-stage formula; used by the transfinite induction in gao_orderAdherence_stage_formula.

theorem OrderClosures.gao_orderAdherence_stage_formula (ξ : Ordinal.{u}) (T : OrderAdherenceTower (GaoStageSet ξ 1)) (β : Ordinal.{u}) : β ≤ ξ → T.stage (Ordinal.lift.{u + 1, u} β) = GaoStageSet ξ (1 + β)

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

theorem OrderClosures.ordinalProjection_strict_stage (ξ γ : Ordinal.{u}) (hγ : γ ≤ ξ) : ∃ (ζ : ↑(GaoIndex ξ)), ordinalProjection ξ ζ ∈ GaoStageSet ξ (γ + 1) ∧ ordinalProjection ξ ζ ∉ GaoStageSet ξ γ

The strict witness separating consecutive stages in Claim 3.