The Cantor-normal-form extension order

def OrderClosures.cnfExtensionLT (ζ ζ' : Ordinal.{u}) : Prop

The relation ≺ from the proof of Theorem thm:solid-iterations, expressed directly using Mathlib's Cantor normal form at base ω.

Equations

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

def OrderClosures.cnfExtensionLE (ζ ζ' : Ordinal.{u}) : Prop

Reflexive closure of the paper's relation ≺.

Equations

• OrderClosures.cnfExtensionLE ζ ζ' = (ζ = ζ' ∨ OrderClosures.cnfExtensionLT ζ ζ')

def OrderClosures.CNFStep (pre : List (Ordinal.{u} × Ordinal.{u})) (x y : Ordinal.{u} × Ordinal.{u}) : Prop

One strict extension after a fixed CNF prefix; introduced separately so transitivity and comparability can be proved before taking transitive closure.

Equations

• OrderClosures.CNFStep pre x y = (y.1 = x.1 ∧ x.2 < y.2 ∨ x.1 < y.1 ∧ (pre = [] ∨ ∃ (z : Ordinal.{?u.1} × Ordinal.{?u.1}), pre.getLast? = some z ∧ y.1 < z.1))

def OrderClosures.CNFListLT (l l' : List (Ordinal.{u} × Ordinal.{u})) : Prop

The transitive closure of one-step CNF extensions; used as a tractable list model of cnfExtensionLT.

Equations

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

noncomputable def OrderClosures.cnfValue (l : List (Ordinal.{u} × Ordinal.{u})) : Ordinal.{u}

Evaluates a list of exponent-coefficient pairs as an ordinal CNF sum; used to compare list extensions with ordinal inequalities.

Equations

• OrderClosures.cnfValue l = List.foldr (fun (p : Ordinal.{?u.1} × Ordinal.{?u.1}) (r : Ordinal.{?u.1}) => Ordinal.omega0 ^ p.1 * p.2 + r) 0 l

theorem OrderClosures.cnfValue_append (l m : List (Ordinal.{u} × Ordinal.{u})) : cnfValue (l ++ m) = cnfValue l + cnfValue m

Computes the ordinal represented by concatenated CNF lists; used in the later comparison lemmas for common prefixes.

theorem OrderClosures.cnfValue_lt_opow (l : List (Ordinal.{u} × Ordinal.{u})) (hsorted : List.Pairwise (fun (a b : Ordinal.{u}) => b < a) (List.map Prod.fst l)) (hcoeff : ∀ p ∈ l, p.2 < Ordinal.omega0) {e : Ordinal.{u}} (hexp : ∀ p ∈ l, p.1 < e) : cnfValue l < Ordinal.omega0 ^ e

Bounds a valid CNF tail by the next larger omega power; used to compare CNF values after extending a common prefix.

theorem OrderClosures.CNF_cnfValue (l : List (Ordinal.{u} × Ordinal.{u})) (hsorted : List.Pairwise (fun (a b : Ordinal.{u}) => b < a) (List.map Prod.fst l)) (hpos : ∀ p ∈ l, 0 < p.2) (hlt : ∀ p ∈ l, p.2 < Ordinal.omega0) : Ordinal.CNF Ordinal.omega0 (cnfValue l) = l

Shows that evaluating the CNF list of an ordinal recovers that ordinal; used to translate between list and ordinal formulations of the extension order.

noncomputable def OrderClosures.cnfAddMonomial (l : List (Ordinal.{u} × Ordinal.{u})) (γ d : Ordinal.{u}) : List (Ordinal.{u} × Ordinal.{u})

Inserts one monomial into a valid CNF list with ordinal-addition semantics; used to construct explicit strict extensions.

Equations

• OrderClosures.cnfAddMonomial [] γ d = [(γ, d)]
• OrderClosures.cnfAddMonomial ((δ, e) :: tail) γ d = if γ < δ then (δ, e) :: OrderClosures.cnfAddMonomial tail γ d else if γ = δ then [(δ, e + d)] else [(γ, d)]

theorem OrderClosures.cnfValue_cnfAddMonomial (l : List (Ordinal.{u} × Ordinal.{u})) (hsorted : List.Pairwise (fun (a b : Ordinal.{u}) => b < a) (List.map Prod.fst l)) (hlt : ∀ p ∈ l, p.2 < Ordinal.omega0) (γ d : Ordinal.{u}) (hd : 0 < d) : cnfValue (cnfAddMonomial l γ d) = cnfValue l + Ordinal.omega0 ^ γ * d

Computes the value after inserting one monomial into a CNF list; used to verify that cnfAddMonomial models ordinal addition.

theorem OrderClosures.cnfAddMonomial_exponents_lt (l : List (Ordinal.{u} × Ordinal.{u})) (γ d δ : Ordinal.{u}) (hl : ∀ p ∈ l, p.1 < δ) (hγ : γ < δ) (p : Ordinal.{u} × Ordinal.{u}) : p ∈ cnfAddMonomial l γ d → p.1 < δ

Preserves the upper exponent bound when adding a monomial; needed for the validity proof of the constructed CNF list.

theorem OrderClosures.cnfAddMonomial_lastExponent (l : List (Ordinal.{u} × Ordinal.{u})) (γ d : Ordinal.{u}) : (Option.map Prod.fst (cnfAddMonomial l γ d).getLast?).getD 0 = γ

Identifies the final exponent after adding a monomial; used to control subsequent extensions of the constructed CNF list.

theorem OrderClosures.cnfAddMonomial_eq_append_of_lt_all (l : List (Ordinal.{u} × Ordinal.{u})) (γ d : Ordinal.{u}) (hγ : ∀ p ∈ l, γ < p.1) : cnfAddMonomial l γ d = l ++ [(γ, d)]

Reduces monomial insertion to list append when its exponent is below all existing exponents; used in the strict-extension construction.

theorem OrderClosures.cnfAddMonomial_valid (l : List (Ordinal.{u} × Ordinal.{u})) (hsorted : List.Pairwise (fun (a b : Ordinal.{u}) => b < a) (List.map Prod.fst l)) (hpos : ∀ p ∈ l, 0 < p.2) (hlt : ∀ p ∈ l, p.2 < Ordinal.omega0) (γ d : Ordinal.{u}) (hdpos : 0 < d) (hdlt : d < Ordinal.omega0) : have out := cnfAddMonomial l γ d; List.Pairwise (fun (a b : Ordinal.{u}) => b < a) (List.map Prod.fst out) ∧ (∀ p ∈ out, 0 < p.2) ∧ ∀ p ∈ out, p.2 < Ordinal.omega0

Proves that monomial insertion preserves CNF validity; this allows its value to be recognized by Mathlib's canonical CNF operation.

theorem OrderClosures.CNF_cnfValue_add_monomial (l : List (Ordinal.{u} × Ordinal.{u})) (hsorted : List.Pairwise (fun (a b : Ordinal.{u}) => b < a) (List.map Prod.fst l)) (hpos : ∀ p ∈ l, 0 < p.2) (hlt : ∀ p ∈ l, p.2 < Ordinal.omega0) (γ d : Ordinal.{u}) (hdpos : 0 < d) (hdlt : d < Ordinal.omega0) : Ordinal.CNF Ordinal.omega0 (cnfValue l + Ordinal.omega0 ^ γ * d) = cnfAddMonomial l γ d

Identifies the canonical CNF of a value with one added monomial; used to construct explicit CNF extensions.

theorem OrderClosures.CNFStep.cons_prefix {pre : List (Ordinal.{u} × Ordinal.{u})} {x y : Ordinal.{u} × Ordinal.{u}} {δ e : Ordinal.{u}} (h : CNFStep pre x y) (hy : y.1 < δ) : CNFStep ((δ, e) :: pre) x y

Adds a common head to a one-step CNF extension; used to lift extensions through arbitrary common prefixes.

theorem OrderClosures.CNFListLT_cnfAddMonomial (l : List (Ordinal.{u} × Ordinal.{u})) (hne : l ≠ []) (hsorted : List.Pairwise (fun (a b : Ordinal.{u}) => b < a) (List.map Prod.fst l)) (hpos : ∀ p ∈ l, 0 < p.2) (hlt : ∀ p ∈ l, p.2 < Ordinal.omega0) (β c : Ordinal.{u}) (hlast : l.getLast? = some (β, c)) (γ d : Ordinal.{u}) (hdpos : 0 < d) (hβγ : β ≤ γ) : CNFListLT l (cnfAddMonomial l γ d)

Shows that adding a sufficiently small monomial gives a strict CNF-list extension; used to approximate ordinals from below.

theorem OrderClosures.cnfValue_append_lt_append (pre l l' : List (Ordinal.{u} × Ordinal.{u})) (h : cnfValue l < cnfValue l') : cnfValue (pre ++ l) < cnfValue (pre ++ l')

Compares values of lists with the same valid prefix; used to show that CNF-list extension implies ordinary ordinal inequality.

theorem OrderClosures.CNFListLT.ordinal_lt {ζ ζ' : Ordinal.{u}} (h : CNFListLT (Ordinal.CNF Ordinal.omega0 ζ) (Ordinal.CNF Ordinal.omega0 ζ')) : ζ < ζ'

Converts strict extension of canonical CNF lists into strict ordinal inequality; used throughout the ordinal-space construction.

theorem OrderClosures.cnfExtensionLT_iff_CNFListLT {ζ ζ' : Ordinal.{u}} : cnfExtensionLT ζ ζ' ↔ CNFListLT (Ordinal.CNF Ordinal.omega0 ζ) (Ordinal.CNF Ordinal.omega0 ζ')

Equates the ordinal definition of cnfExtensionLT with its list model; this bridge supplies transitivity and upper-cone linearity.

theorem OrderClosures.cnfExtensionLT_add_singleton_of_last {ζ q γ d β c : Ordinal.{u}} {pre : List (Ordinal.{u} × Ordinal.{u})} (hζ : Ordinal.CNF Ordinal.omega0 ζ = pre ++ [(β, c)]) (hq : Ordinal.CNF Ordinal.omega0 q = [(γ, d)]) (hβγ : β ≤ γ) : cnfExtensionLT ζ (ζ + q)

Appending one smaller singleton monomial creates a strict CNF extension; used in the later Gao-stage approximation argument.

theorem OrderClosures.CNFStep.trans {pre : List (Ordinal.{u} × Ordinal.{u})} {x y z : Ordinal.{u} × Ordinal.{u}} (hxy : CNFStep pre x y) (hyz : CNFStep pre y z) : CNFStep pre x z

Proves transitivity for one-step extensions sharing a prefix; used in the global transitivity proof for CNFListLT.

theorem OrderClosures.CNFStep.trichotomy {pre : List (Ordinal.{u} × Ordinal.{u})} {x y z : Ordinal.{u} × Ordinal.{u}} (hxy : CNFStep pre x y) (hxz : CNFStep pre x z) : y = z ∨ CNFStep pre y z ∨ CNFStep pre z y

Establishes comparability of two one-step extensions above a common prefix; used to linearize each upper cone.

theorem OrderClosures.CNFListLT.trans {l m n : List (Ordinal.{u} × Ordinal.{u})} (hlm : CNFListLT l m) (hmn : CNFListLT m n) : CNFListLT l n

Lifts one-step transitivity to the transitive closure CNFListLT; used to prove that cnfExtensionLE is a partial order.

theorem OrderClosures.CNFListLT.upper_trichotomy {l m n : List (Ordinal.{u} × Ordinal.{u})} (hlm : CNFListLT l m) (hln : CNFListLT l n) : m = n ∨ CNFListLT m n ∨ CNFListLT n m

Shows that two CNF lists extending a fixed list are comparable; used for linearity of upper cones in the ordinal extension order.

theorem OrderClosures.cnfExtensionLE_partialOrder_and_subrelation : IsPartialOrder Ordinal.{u} cnfExtensionLE ∧ ∀ {ζ ζ' : Ordinal.{u}}, cnfExtensionLE ζ ζ' → ζ ≤ ζ'

Property P1 of the ordinal relation in the proof of thm:solid-iterations.

theorem OrderClosures.cnfExtensionLT_linear_above (ζ : Ordinal.{u}) {η η' : Ordinal.{u}} : cnfExtensionLT ζ η → cnfExtensionLT ζ η' → (cnfExtensionLT η η' ↔ η < η')

Property P2 of the ordinal relation in the proof of thm:solid-iterations.

theorem OrderClosures.cnfExtensionLE_linear_above (ζ : Ordinal.{u}) {η η' : Ordinal.{u}} (hη : cnfExtensionLE ζ η) (hη' : cnfExtensionLE ζ η') : cnfExtensionLE η η' ∨ cnfExtensionLE η' η

Includes equality in upper-cone comparability; used when minimal Gao dominators must be compared in StageFormula.