From 968320e834eb2f7d4cc111909099b0d7ae51100c Mon Sep 17 00:00:00 2001 From: Tim B Date: Fri, 9 Oct 2026 11:28:45 -0500 Subject: [PATCH 1/3] theta_0 0 is the least fixed point of omega^. on ThetaWNoteD, and the supremum of the omega-tower over 0 New module OrdinalAnalysis/Ordinal/ThetaW/EpsilonZero.lean. On the domained multi-level theta-notation, isLeast_epsilonZero shows that theta_0 0 is the least fixed point of omegaPow, and lt_epsilonZero_iff shows that a notation lies below theta_0 0 exactly when it lies below some stage omegaTower m 0. Both are stated against the notation's own order and omegaPow, reuse omegaTower from HullCofinal.lean, and do not use well-foundedness. The two theorems are added to scripts/AxiomCheck.lean and the README's ThetaWNoteD paragraph mentions them. Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01FJrffXdNS9Weh7DwnUt9PV --- OrdinalAnalysis.lean | 1 + .../Ordinal/ThetaW/EpsilonZero.lean | 152 ++++++++++++++++++ README.md | 4 +- scripts/AxiomCheck.lean | 6 + 4 files changed, 162 insertions(+), 1 deletion(-) create mode 100644 OrdinalAnalysis/Ordinal/ThetaW/EpsilonZero.lean diff --git a/OrdinalAnalysis.lean b/OrdinalAnalysis.lean index 55b8023..178a6d5 100644 --- a/OrdinalAnalysis.lean +++ b/OrdinalAnalysis.lean @@ -361,6 +361,7 @@ import OrdinalAnalysis.IDn.AxiomsIDCases.xFreeI_predOf import OrdinalAnalysis.IDn.CollapseCorollary import OrdinalAnalysis.IDn.EmbedHypsReplace import OrdinalAnalysis.Ordinal.ThetaW.TowerCofinal +import OrdinalAnalysis.Ordinal.ThetaW.EpsilonZero import OrdinalAnalysis.IDn.LowerSharp import OrdinalAnalysis.IDn.AxiomsIDCases.plugI_subst_numI import OrdinalAnalysis.IDn.TautAdditive diff --git a/OrdinalAnalysis/Ordinal/ThetaW/EpsilonZero.lean b/OrdinalAnalysis/Ordinal/ThetaW/EpsilonZero.lean new file mode 100644 index 0000000..74bd6a8 --- /dev/null +++ b/OrdinalAnalysis/Ordinal/ThetaW/EpsilonZero.lean @@ -0,0 +1,152 @@ +/- + `ϑ₀ 0` is the least fixed point of `ω^·` on the domained multi-level ϑ-notation, and the + supremum of the ω-tower over `0`. + + On `ThetaWNoteD` the fixed points of `omegaPow` are exactly the principal terms + (`omegaPow_eq_self_iff`), so `ϑ₀ 0` is a fixed point by the normal form. This file adds the + two facts that make `ϑ₀ 0` the notation's own `ε₀`, stated against the notation's order and + its own `omegaPow`, with no reading into `Ordinal`: + + * `isLeast_epsilonZero`: `ϑ₀ 0` is the *least* fixed point of `omegaPow`. Every other + principal term is `Ω_j`, `ϑ_j β` with `j > 0`, or `ϑ₀ β` with `β ≠ 0`, and each of these + lies above `ϑ₀ 0` by a clause of the raw term order (`theta_lt_Omega_iff`, + `theta_lt_theta_of_lt_level`, `theta_lt_theta_of_lt`). Well-foundedness is not used. + * `exists_lt_omegaTower_of_lt_epsilonZero`: every notation below `ϑ₀ 0` lies below + `ω_m(0)` for some `m` (`omegaTower`, `HullCofinal.lean`), and conversely every `ω_m(0)` + lies below `ϑ₀ 0` (`omegaTower_zero_lt_epsilonZero`). The proof is induction on the term + length: a notation below `ϑ₀ 0` is not principal (by leastness), so it is a Cantor sum whose + entries lie below `ϑ₀ 0` (`lt_prin_iff`), each entry is below some stage by induction, and + the sum lies below `ω^·` of the largest of those stages (`lt_omegaPow_iff`). +-/ +import OrdinalAnalysis.Ordinal.ThetaW.HullCofinal + +set_option autoImplicit false + +namespace OrdinalAnalysis + +namespace ThetaWNoteD + +open ThetaWTerm + +/-! ### The notation `ϑ₀ 0` -/ + +theorem dom_theta_zero_zero : ThetaWTerm.Dom (ThetaWTerm.theta 0 ThetaWTerm.zero) := + ThetaWTerm.dom_theta_of_G_nil ThetaWTerm.dom_zero (ThetaWTerm.G_nil 0) + +/-- `ϑ₀ 0`, the notation for `ε₀`. -/ +def epsilonZero : ThetaWNoteD := + ⟨ThetaWTerm.theta 0 ThetaWTerm.zero, + (ThetaWTerm.nf_theta_iff _ _).mpr ThetaWTerm.nf_zero, dom_theta_zero_zero⟩ + +theorem epsilonZero_val : epsilonZero.1 = ThetaWTerm.theta 0 ThetaWTerm.zero := rfl + +theorem isPrin_epsilonZero : ThetaWTerm.IsPrin epsilonZero.1 := trivial + +/-! ### `ϑ₀ 0` is the least fixed point of `omegaPow` -/ + +/-- `ω^(ϑ₀ 0) = ϑ₀ 0`. -/ +theorem omegaPow_epsilonZero : omegaPow epsilonZero = epsilonZero := + omegaPow_eq_self_iff.mpr isPrin_epsilonZero + +/-- Every fixed point of `omegaPow` lies at or above `ϑ₀ 0`. -/ +theorem epsilonZero_le_of_omegaPow_eq {a : ThetaWNoteD} (h : omegaPow a = a) : + epsilonZero ≤ a := by + have hp : ThetaWTerm.IsPrin a.1 := omegaPow_eq_self_iff.mp h + rw [le_iff] + obtain ⟨t, hnf, hdom⟩ := a + show ThetaWTerm.theta 0 ThetaWTerm.zero ≤ t + cases t with + | Omega j => exact Or.inl ((ThetaWTerm.theta_lt_Omega_iff 0 j _).mpr (Nat.zero_le j)) + | theta j b => + rcases Nat.eq_zero_or_pos j with rfl | hj + · by_cases hb : b = ThetaWTerm.sum [] + · subst hb; exact Or.inr rfl + · left + apply ThetaWTerm.theta_lt_theta_of_lt (ThetaWTerm.nil_lt_of_ne hb) + intro g hg + simp at hg + · exact Or.inl (ThetaWTerm.theta_lt_theta_of_lt_level _ _ hj) + | sum xs => exact absurd hp id + +/-- **`ϑ₀ 0` is the least fixed point of `ω^·`.** -/ +theorem isLeast_epsilonZero : IsLeast {a : ThetaWNoteD | omegaPow a = a} epsilonZero := + ⟨omegaPow_epsilonZero, fun _ ha => epsilonZero_le_of_omegaPow_eq ha⟩ + +/-- No notation below `ϑ₀ 0` is a fixed point of `ω^·`. -/ +theorem omegaPow_ne_self_of_lt_epsilonZero {a : ThetaWNoteD} (ha : a < epsilonZero) : + omegaPow a ≠ a := + fun h => absurd (epsilonZero_le_of_omegaPow_eq h) (not_le.mpr ha) + +/-! ### `ϑ₀ 0` is the supremum of the ω-tower over `0` -/ + +theorem omegaTower_zero_lt_succ : ∀ m : ℕ, omegaTower m zero < omegaTower (m + 1) zero + | 0 => zero_lt_one + | m + 1 => omegaPow_lt_omegaPow (omegaTower_zero_lt_succ m) + +theorem omegaTower_zero_mono {m₁ m₂ : ℕ} (h : m₁ ≤ m₂) : + omegaTower m₁ zero ≤ omegaTower m₂ zero := by + induction h with + | refl => exact le_rfl + | step _ ih => exact le_trans ih (le_of_lt (omegaTower_zero_lt_succ _)) + +/-- Every stage `ω_m(0)` of the tower lies below `ϑ₀ 0`. -/ +theorem omegaTower_zero_lt_epsilonZero : ∀ m : ℕ, omegaTower m zero < epsilonZero + | 0 => lt_iff.mpr (ThetaWTerm.nil_lt_theta 0 _) + | m + 1 => omegaPow_lt_prin (p := epsilonZero) isPrin_epsilonZero + (omegaTower_zero_lt_epsilonZero m) + +/-- A finite list of terms, each below some stage of the tower, lies below a single stage. -/ +theorem exists_omegaTower_zero_bound (xs : List ThetaWTerm) + (h : ∀ e ∈ xs, ∃ m, e < (omegaTower m zero).1) : + ∃ M, ∀ e ∈ xs, e < (omegaTower M zero).1 := by + induction xs with + | nil => exact ⟨0, by simp⟩ + | cons x xs ih => + obtain ⟨m, hm⟩ := h x (by simp) + obtain ⟨M, hM⟩ := ih (fun e he => h e (by simp [he])) + refine ⟨max m M, ?_⟩ + intro e he + rcases List.mem_cons.mp he with rfl | he + · exact ThetaWTerm.lt_of_lt_of_le' hm (le_iff.mp (omegaTower_zero_mono (le_max_left _ _))) + · exact ThetaWTerm.lt_of_lt_of_le' (hM e he) + (le_iff.mp (omegaTower_zero_mono (le_max_right _ _))) + +theorem exists_lt_omegaTower_of_lt_epsilonZero_aux (N : ℕ) : + ∀ a : ThetaWNoteD, ThetaWTerm.l a.1 ≤ N → a < epsilonZero → + ∃ m, a < omegaTower m zero := by + induction N using Nat.strong_induction_on with + | _ N ih => + intro a hl ha + have hnp : ¬ ThetaWTerm.IsPrin a.1 := fun hp => + omegaPow_ne_self_of_lt_epsilonZero ha (omegaPow_eq_self_iff.mpr hp) + have hbelow := (lt_prin_iff (p := epsilonZero) isPrin_epsilonZero).mp ha + have hent : ∀ e ∈ a.entries, ∃ m, e < (omegaTower m zero).1 := by + intro e he + obtain ⟨t, hnf, hdom⟩ := a + cases t with + | Omega k => exact absurd trivial hnp + | theta k b => exact absurd trivial hnp + | sum xs => + have hex : e ∈ xs := he + have hle : ThetaWTerm.l e < N := lt_of_lt_of_le (ThetaWTerm.l_lt_of_mem hex) hl + let e' : ThetaWNoteD := + ⟨e, (cnf_entries ⟨_, hnf, hdom⟩).nf he, dom_entries ⟨_, hnf, hdom⟩ e he⟩ + exact ih (ThetaWTerm.l e) hle e' le_rfl (hbelow e he) + obtain ⟨M, hM⟩ := exists_omegaTower_zero_bound a.entries hent + exact ⟨M + 1, lt_omegaPow_iff.mpr hM⟩ + +/-- **`ϑ₀ 0` is the supremum of `0, ω^0, ω^ω^0, …`**: every notation below it lies below +some stage of the tower. -/ +theorem exists_lt_omegaTower_of_lt_epsilonZero {a : ThetaWNoteD} (ha : a < epsilonZero) : + ∃ m, a < omegaTower m zero := + exists_lt_omegaTower_of_lt_epsilonZero_aux _ a le_rfl ha + +/-- Below `ϑ₀ 0` means below some stage of the ω-tower over `0`. -/ +theorem lt_epsilonZero_iff {a : ThetaWNoteD} : + a < epsilonZero ↔ ∃ m, a < omegaTower m zero := + ⟨exists_lt_omegaTower_of_lt_epsilonZero, + fun ⟨m, hm⟩ => lt_trans hm (omegaTower_zero_lt_epsilonZero m)⟩ + +end ThetaWNoteD + +end OrdinalAnalysis diff --git a/README.md b/README.md index 0c85600..7b17b22 100644 --- a/README.md +++ b/README.md @@ -556,7 +556,9 @@ theta-functions*, Math. Log. Quart. 57, Definition 2.7 and Proposition 2.15). Th restriction, not a formality: `ThetaWNoteD.wellFoundedLT` (`WellFoundedD.lean`) holds for the domained order, while the same syntax without the domain guard, `ThetaWNote`, is *not* well-founded (`Descent.lean`'s `not_wellFoundedLT`, an explicit infinite descending sequence). -`c n = ϑ₀(ϑ_n 0)` (`Dom.lean`) is the domained term for the intended value of `|ID_n|`. Above the +`c n = ϑ₀(ϑ_n 0)` (`Dom.lean`) is the domained term for the intended value of `|ID_n|`. `EpsilonZero.lean` shows that `ϑ₀ 0` is the notation's own `ε₀`: it is the least fixed +point of the notation's `ω^·` (`isLeast_epsilonZero`) and the supremum of the ω-tower over `0` +(`lt_epsilonZero_iff`). Above the raw system, `HullSingle.lean` proves the level-free hull operator is least (`theta_isLeastS`, Wilken's Proposition 3.9 at every level at once), and `HullDom.lean` derives the domain lemma the collapsing theorem needs from it (`dom_add_omegaPow`) while also recording where the audited diff --git a/scripts/AxiomCheck.lean b/scripts/AxiomCheck.lean index fee0f2e..3ac8bf5 100644 --- a/scripts/AxiomCheck.lean +++ b/scripts/AxiomCheck.lean @@ -1477,6 +1477,12 @@ info: 'OrdinalAnalysis.InductiveDef.UpperBound.tiUptoSentence_Omega' depends on /-- info: 'OrdinalAnalysis.ThetaWNoteD.wellFoundedLT' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms OrdinalAnalysis.ThetaWNoteD.wellFoundedLT +/-- info: 'OrdinalAnalysis.ThetaWNoteD.isLeast_epsilonZero' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in #print axioms OrdinalAnalysis.ThetaWNoteD.isLeast_epsilonZero + +/-- info: 'OrdinalAnalysis.ThetaWNoteD.lt_epsilonZero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in #print axioms OrdinalAnalysis.ThetaWNoteD.lt_epsilonZero_iff + /-- info: 'OrdinalAnalysis.ThetaWNoteD.dom_add' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms OrdinalAnalysis.ThetaWNoteD.dom_add From 800e42c2f0f8f75fc13b766b0ed088a4125291e9 Mon Sep 17 00:00:00 2001 From: Tim B Date: Fri, 16 Oct 2026 23:36:39 -0500 Subject: [PATCH 2/3] theta 0 on ThetaNote: least fixed point of omega^. and supremum of the omega-tower; raw-term leastness on both notations New module OrdinalAnalysis/Ordinal/Theta/EpsilonZero.lean, the one-level counterpart of Ordinal/ThetaW/EpsilonZero.lean: ThetaNote.isLeast_epsilonZero and ThetaNote.lt_epsilonZero_iff. On both notations leastness now rests on a raw-term lemma, ThetaTerm.theta_zero_le_of_ofList_eq and ThetaWTerm.theta_zero_zero_le_of_ofList_eq (ofList [t] = t implies theta 0 <= t, with no normal-form or domain hypothesis), proved by cases from the existing order clauses; both use only propext and Quot.sound. The import, the AxiomCheck entries (raw lemmas pinned at [propext, Quot.sound]) and a README mention are added. Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01FJrffXdNS9Weh7DwnUt9PV --- OrdinalAnalysis.lean | 1 + .../Ordinal/Theta/EpsilonZero.lean | 157 ++++++++++++++++++ .../Ordinal/ThetaW/EpsilonZero.lean | 57 ++++--- README.md | 3 +- scripts/AxiomCheck.lean | 12 ++ 5 files changed, 208 insertions(+), 22 deletions(-) create mode 100644 OrdinalAnalysis/Ordinal/Theta/EpsilonZero.lean diff --git a/OrdinalAnalysis.lean b/OrdinalAnalysis.lean index 178a6d5..eca53cc 100644 --- a/OrdinalAnalysis.lean +++ b/OrdinalAnalysis.lean @@ -209,6 +209,7 @@ import OrdinalAnalysis.Ordinal.Theta.Instance import OrdinalAnalysis.Ordinal.Theta.WellFounded import OrdinalAnalysis.Ordinal.Theta.Hull import OrdinalAnalysis.Ordinal.Theta.HullCofinal +import OrdinalAnalysis.Ordinal.Theta.EpsilonZero import OrdinalAnalysis.ID1.Language import OrdinalAnalysis.ID1.Rank import OrdinalAnalysis.ID1.Internal.CovTable diff --git a/OrdinalAnalysis/Ordinal/Theta/EpsilonZero.lean b/OrdinalAnalysis/Ordinal/Theta/EpsilonZero.lean new file mode 100644 index 0000000..eac2458 --- /dev/null +++ b/OrdinalAnalysis/Ordinal/Theta/EpsilonZero.lean @@ -0,0 +1,157 @@ +/- + `ϑ 0` is the least fixed point of `ω^·` on the one-level ϑ-notation, and the supremum of the + ω-tower over `0`. + + The one-level counterpart of `Ordinal/ThetaW/EpsilonZero.lean`. On `ThetaNote` the fixed + points of `omegaPow` are exactly the principal terms (`omegaPow_eq_self_iff`), so `ϑ 0` is a + fixed point by the normal form. This file adds the two facts that make `ϑ 0` the notation's + own `ε₀`, stated against the notation's order and its own `omegaPow`, with no reading into + `Ordinal`: + + * `isLeast_epsilonZero`: `ϑ 0` is the *least* fixed point of `omegaPow`. It rests on the + raw-term form `ThetaTerm.theta_zero_le_of_ofList_eq` (every term `t` with `ofList [t] = t` + satisfies `ϑ 0 ≤ t`, no normal-form hypothesis): such a `t` is `Ω` or `ϑ β`, and both lie at + or above `ϑ 0` by a clause of the raw term order (`theta_lt_Omega`, `theta_lt_theta_of_lt`). + Well-foundedness is not used, and the raw form uses no `Classical.choice`. + * `lt_epsilonZero_iff`: a notation lies below `ϑ 0` exactly when it lies below `ω_m(0)` for + some `m` (`omegaTower`, `HullCofinal.lean`). The proof is induction on the term length: a + notation below `ϑ 0` is not principal (by leastness), so it is a Cantor sum whose entries + lie below `ϑ 0` (`lt_prin_iff`), each entry is below some stage by induction, and the sum + lies below `ω^·` of the largest of those stages (`lt_omegaPow_iff`). +-/ +import OrdinalAnalysis.Ordinal.Theta.HullCofinal + +set_option autoImplicit false + +namespace OrdinalAnalysis + +namespace ThetaTerm + +/-- Raw form of leastness: every term that `ofList [·]` fixes lies at or above `ϑ 0`. -/ +theorem theta_zero_le_of_ofList_eq {t : ThetaTerm} (h : ofList [t] = t) : + theta zero ≤ t := by + cases t with + | Omega => exact Or.inl (theta_lt_Omega _) + | theta b => + by_cases hb : b = sum [] + · subst hb; exact Or.inr rfl + · left + apply theta_lt_theta_of_lt (nil_lt_of_ne hb) + intro g hg + simp at hg + | sum xs => + exfalso + have hof : ofList [sum xs] = sum [sum xs] := rfl + rw [hof] at h + injection h with h + have := congrArg sizeOf h + simp at this + omega + +end ThetaTerm + +namespace ThetaNote + +open ThetaTerm + +/-! ### The notation `ϑ 0` -/ + +/-- `ϑ 0`, the notation for `ε₀`. -/ +def epsilonZero : ThetaNote := theta zero + +theorem epsilonZero_val : epsilonZero.1 = ThetaTerm.theta ThetaTerm.zero := rfl + +theorem isPrin_epsilonZero : ThetaTerm.IsPrin epsilonZero.1 := trivial + +/-! ### `ϑ 0` is the least fixed point of `omegaPow` -/ + +/-- `ω^(ϑ 0) = ϑ 0`. -/ +theorem omegaPow_epsilonZero : omegaPow epsilonZero = epsilonZero := + omegaPow_eq_self_iff.mpr isPrin_epsilonZero + +/-- Every fixed point of `omegaPow` lies at or above `ϑ 0`. -/ +theorem epsilonZero_le_of_omegaPow_eq {a : ThetaNote} (h : omegaPow a = a) : + epsilonZero ≤ a := + le_iff.mpr (ThetaTerm.theta_zero_le_of_ofList_eq (congrArg Subtype.val h)) + +/-- **`ϑ 0` is the least fixed point of `ω^·`.** -/ +theorem isLeast_epsilonZero : IsLeast {a : ThetaNote | omegaPow a = a} epsilonZero := + ⟨omegaPow_epsilonZero, fun _ ha => epsilonZero_le_of_omegaPow_eq ha⟩ + +/-- No notation below `ϑ 0` is a fixed point of `ω^·`. -/ +theorem omegaPow_ne_self_of_lt_epsilonZero {a : ThetaNote} (ha : a < epsilonZero) : + omegaPow a ≠ a := + fun h => absurd (epsilonZero_le_of_omegaPow_eq h) (not_le.mpr ha) + +/-! ### `ϑ 0` is the supremum of the ω-tower over `0` -/ + +theorem omegaTower_zero_lt_succ : ∀ m : ℕ, omegaTower m zero < omegaTower (m + 1) zero + | 0 => zero_lt_one + | m + 1 => omegaPow_lt_omegaPow (omegaTower_zero_lt_succ m) + +theorem omegaTower_zero_mono {m₁ m₂ : ℕ} (h : m₁ ≤ m₂) : + omegaTower m₁ zero ≤ omegaTower m₂ zero := by + induction h with + | refl => exact le_rfl + | step _ ih => exact le_trans ih (le_of_lt (omegaTower_zero_lt_succ _)) + +/-- Every stage `ω_m(0)` of the tower lies below `ϑ 0`. -/ +theorem omegaTower_zero_lt_epsilonZero : ∀ m : ℕ, omegaTower m zero < epsilonZero + | 0 => lt_iff.mpr (ThetaTerm.nil_lt_theta _) + | m + 1 => omegaPow_lt_prin (p := epsilonZero) isPrin_epsilonZero + (omegaTower_zero_lt_epsilonZero m) + +/-- A finite list of terms, each below some stage of the tower, lies below a single stage. -/ +theorem exists_omegaTower_zero_bound (xs : List ThetaTerm) + (h : ∀ e ∈ xs, ∃ m, e < (omegaTower m zero).1) : + ∃ M, ∀ e ∈ xs, e < (omegaTower M zero).1 := by + induction xs with + | nil => exact ⟨0, by simp⟩ + | cons x xs ih => + obtain ⟨m, hm⟩ := h x (by simp) + obtain ⟨M, hM⟩ := ih (fun e he => h e (by simp [he])) + refine ⟨max m M, ?_⟩ + intro e he + rcases List.mem_cons.mp he with rfl | he + · exact ThetaTerm.lt_of_lt_of_le' hm (le_iff.mp (omegaTower_zero_mono (le_max_left _ _))) + · exact ThetaTerm.lt_of_lt_of_le' (hM e he) + (le_iff.mp (omegaTower_zero_mono (le_max_right _ _))) + +theorem exists_lt_omegaTower_of_lt_epsilonZero_aux (N : ℕ) : + ∀ a : ThetaNote, ThetaTerm.l a.1 ≤ N → a < epsilonZero → + ∃ m, a < omegaTower m zero := by + induction N using Nat.strong_induction_on with + | _ N ih => + intro a hl ha + have hnp : ¬ ThetaTerm.IsPrin a.1 := fun hp => + omegaPow_ne_self_of_lt_epsilonZero ha (omegaPow_eq_self_iff.mpr hp) + have hbelow := (lt_prin_iff (p := epsilonZero) isPrin_epsilonZero).mp ha + have hent : ∀ e ∈ a.entries, ∃ m, e < (omegaTower m zero).1 := by + intro e he + obtain ⟨t, hnf⟩ := a + cases t with + | Omega => exact absurd trivial hnp + | theta b => exact absurd trivial hnp + | sum xs => + have hex : e ∈ xs := he + have hle : ThetaTerm.l e < N := lt_of_lt_of_le (ThetaTerm.l_lt_of_mem hex) hl + let e' : ThetaNote := ⟨e, (cnf_entries ⟨_, hnf⟩).nf he⟩ + exact ih (ThetaTerm.l e) hle e' le_rfl (hbelow e he) + obtain ⟨M, hM⟩ := exists_omegaTower_zero_bound a.entries hent + exact ⟨M + 1, lt_omegaPow_iff.mpr hM⟩ + +/-- **`ϑ 0` is the supremum of `0, ω^0, ω^ω^0, …`**: every notation below it lies below some +stage of the tower. -/ +theorem exists_lt_omegaTower_of_lt_epsilonZero {a : ThetaNote} (ha : a < epsilonZero) : + ∃ m, a < omegaTower m zero := + exists_lt_omegaTower_of_lt_epsilonZero_aux _ a le_rfl ha + +/-- Below `ϑ 0` means below some stage of the ω-tower over `0`. -/ +theorem lt_epsilonZero_iff {a : ThetaNote} : + a < epsilonZero ↔ ∃ m, a < omegaTower m zero := + ⟨exists_lt_omegaTower_of_lt_epsilonZero, + fun ⟨m, hm⟩ => lt_trans hm (omegaTower_zero_lt_epsilonZero m)⟩ + +end ThetaNote + +end OrdinalAnalysis diff --git a/OrdinalAnalysis/Ordinal/ThetaW/EpsilonZero.lean b/OrdinalAnalysis/Ordinal/ThetaW/EpsilonZero.lean index 74bd6a8..5b066a3 100644 --- a/OrdinalAnalysis/Ordinal/ThetaW/EpsilonZero.lean +++ b/OrdinalAnalysis/Ordinal/ThetaW/EpsilonZero.lean @@ -7,10 +7,13 @@ two facts that make `ϑ₀ 0` the notation's own `ε₀`, stated against the notation's order and its own `omegaPow`, with no reading into `Ordinal`: - * `isLeast_epsilonZero`: `ϑ₀ 0` is the *least* fixed point of `omegaPow`. Every other - principal term is `Ω_j`, `ϑ_j β` with `j > 0`, or `ϑ₀ β` with `β ≠ 0`, and each of these - lies above `ϑ₀ 0` by a clause of the raw term order (`theta_lt_Omega_iff`, - `theta_lt_theta_of_lt_level`, `theta_lt_theta_of_lt`). Well-foundedness is not used. + * `isLeast_epsilonZero`: `ϑ₀ 0` is the *least* fixed point of `omegaPow`. It rests on the + raw-term form `ThetaWTerm.theta_zero_zero_le_of_ofList_eq` (every term `t` with + `ofList [t] = t` satisfies `ϑ₀ 0 ≤ t`, no normal-form or domain hypothesis): such a `t` is + `Ω_j`, `ϑ_j β` with `j > 0`, or `ϑ₀ β`, and each of these lies at or above `ϑ₀ 0` by a + clause of the raw term order (`theta_lt_Omega_iff`, `theta_lt_theta_of_lt_level`, + `theta_lt_theta_of_lt`). Well-foundedness is not used, and the raw form uses no + `Classical.choice`. * `exists_lt_omegaTower_of_lt_epsilonZero`: every notation below `ϑ₀ 0` lies below `ω_m(0)` for some `m` (`omegaTower`, `HullCofinal.lean`), and conversely every `ω_m(0)` lies below `ϑ₀ 0` (`omegaTower_zero_lt_epsilonZero`). The proof is induction on the term @@ -24,6 +27,33 @@ set_option autoImplicit false namespace OrdinalAnalysis +namespace ThetaWTerm + +/-- Raw form of leastness: every term that `ofList [·]` fixes lies at or above `ϑ₀ 0`. -/ +theorem theta_zero_zero_le_of_ofList_eq {t : ThetaWTerm} (h : ofList [t] = t) : + theta 0 zero ≤ t := by + cases t with + | Omega j => exact Or.inl ((theta_lt_Omega_iff 0 j _).mpr (Nat.zero_le j)) + | theta j b => + rcases Nat.eq_zero_or_pos j with rfl | hj + · by_cases hb : b = sum [] + · subst hb; exact Or.inr rfl + · left + apply theta_lt_theta_of_lt (nil_lt_of_ne hb) + intro g hg + simp at hg + · exact Or.inl (theta_lt_theta_of_lt_level _ _ hj) + | sum xs => + exfalso + have hof : ofList [sum xs] = sum [sum xs] := rfl + rw [hof] at h + injection h with h + have := congrArg sizeOf h + simp at this + omega + +end ThetaWTerm + namespace ThetaWNoteD open ThetaWTerm @@ -50,23 +80,8 @@ theorem omegaPow_epsilonZero : omegaPow epsilonZero = epsilonZero := /-- Every fixed point of `omegaPow` lies at or above `ϑ₀ 0`. -/ theorem epsilonZero_le_of_omegaPow_eq {a : ThetaWNoteD} (h : omegaPow a = a) : - epsilonZero ≤ a := by - have hp : ThetaWTerm.IsPrin a.1 := omegaPow_eq_self_iff.mp h - rw [le_iff] - obtain ⟨t, hnf, hdom⟩ := a - show ThetaWTerm.theta 0 ThetaWTerm.zero ≤ t - cases t with - | Omega j => exact Or.inl ((ThetaWTerm.theta_lt_Omega_iff 0 j _).mpr (Nat.zero_le j)) - | theta j b => - rcases Nat.eq_zero_or_pos j with rfl | hj - · by_cases hb : b = ThetaWTerm.sum [] - · subst hb; exact Or.inr rfl - · left - apply ThetaWTerm.theta_lt_theta_of_lt (ThetaWTerm.nil_lt_of_ne hb) - intro g hg - simp at hg - · exact Or.inl (ThetaWTerm.theta_lt_theta_of_lt_level _ _ hj) - | sum xs => exact absurd hp id + epsilonZero ≤ a := + le_iff.mpr (ThetaWTerm.theta_zero_zero_le_of_ofList_eq (congrArg Subtype.val h)) /-- **`ϑ₀ 0` is the least fixed point of `ω^·`.** -/ theorem isLeast_epsilonZero : IsLeast {a : ThetaWNoteD | omegaPow a = a} epsilonZero := diff --git a/README.md b/README.md index 7b17b22..b3c6d3d 100644 --- a/README.md +++ b/README.md @@ -498,7 +498,8 @@ Buchholz's notation `OT_B` below `ψ₀(Ω_ω)`, in Lean 4 and Isabelle, exists koteitan's `pss-proof` (2026), so this is not the first such proof — what is new here, as far as the surveys reach, is the ordinal analysis built on it), the hull sets and operators -(`Hull.lean`, `HullCofinal.lean`); the theory `ID₁` and its consistency by the +(`Hull.lean`, `HullCofinal.lean`); `ϑ 0` as the notation's own `ε₀`, the least fixed point of its +`ω^·` and the supremum of the ω-tower over `0` (`EpsilonZero.lean`); the theory `ID₁` and its consistency by the least fixed point (`ID1/{Theory,Sound}.lean`); the coding of the notation in arithmetic with the order facts inside `IΣ₁` (`ID1/Internal/`); the stage language and rank (`Language.lean`, `Rank.lean`); the operator-controlled diff --git a/scripts/AxiomCheck.lean b/scripts/AxiomCheck.lean index 3ac8bf5..43936fa 100644 --- a/scripts/AxiomCheck.lean +++ b/scripts/AxiomCheck.lean @@ -1483,6 +1483,18 @@ info: 'OrdinalAnalysis.InductiveDef.UpperBound.tiUptoSentence_Omega' depends on /-- info: 'OrdinalAnalysis.ThetaWNoteD.lt_epsilonZero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms OrdinalAnalysis.ThetaWNoteD.lt_epsilonZero_iff +/-- info: 'OrdinalAnalysis.ThetaNote.isLeast_epsilonZero' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in #print axioms OrdinalAnalysis.ThetaNote.isLeast_epsilonZero + +/-- info: 'OrdinalAnalysis.ThetaNote.lt_epsilonZero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in #print axioms OrdinalAnalysis.ThetaNote.lt_epsilonZero_iff + +/-- info: 'OrdinalAnalysis.ThetaWTerm.theta_zero_zero_le_of_ofList_eq' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in #print axioms OrdinalAnalysis.ThetaWTerm.theta_zero_zero_le_of_ofList_eq + +/-- info: 'OrdinalAnalysis.ThetaTerm.theta_zero_le_of_ofList_eq' depends on axioms: [propext, Quot.sound] -/ +#guard_msgs in #print axioms OrdinalAnalysis.ThetaTerm.theta_zero_le_of_ofList_eq + /-- info: 'OrdinalAnalysis.ThetaWNoteD.dom_add' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms OrdinalAnalysis.ThetaWNoteD.dom_add From d959cfc06c15c17141edae9b5a6ee6f82034d6b5 Mon Sep 17 00:00:00 2001 From: Tim B Date: Fri, 16 Oct 2026 23:38:32 -0500 Subject: [PATCH 3/3] README: rewrap the EpsilonZero mentions to the surrounding line width Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01FJrffXdNS9Weh7DwnUt9PV --- README.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index b3c6d3d..8d166d7 100644 --- a/README.md +++ b/README.md @@ -498,9 +498,10 @@ Buchholz's notation `OT_B` below `ψ₀(Ω_ω)`, in Lean 4 and Isabelle, exists koteitan's `pss-proof` (2026), so this is not the first such proof — what is new here, as far as the surveys reach, is the ordinal analysis built on it), the hull sets and operators -(`Hull.lean`, `HullCofinal.lean`); `ϑ 0` as the notation's own `ε₀`, the least fixed point of its -`ω^·` and the supremum of the ω-tower over `0` (`EpsilonZero.lean`); the theory `ID₁` and its consistency by the -least fixed point (`ID1/{Theory,Sound}.lean`); the coding of the notation in +(`Hull.lean`, `HullCofinal.lean`); `ϑ 0` as the least fixed point of `ω^·` and +the supremum of the ω-tower over `0` (`EpsilonZero.lean`); the theory `ID₁` and +its consistency by the least fixed point (`ID1/{Theory,Sound}.lean`); the +coding of the notation in arithmetic with the order facts inside `IΣ₁` (`ID1/Internal/`); the stage language and rank (`Language.lean`, `Rank.lean`); the operator-controlled infinitary calculus with the stage rules, the boundedness lemma and the @@ -557,9 +558,9 @@ theta-functions*, Math. Log. Quart. 57, Definition 2.7 and Proposition 2.15). Th restriction, not a formality: `ThetaWNoteD.wellFoundedLT` (`WellFoundedD.lean`) holds for the domained order, while the same syntax without the domain guard, `ThetaWNote`, is *not* well-founded (`Descent.lean`'s `not_wellFoundedLT`, an explicit infinite descending sequence). -`c n = ϑ₀(ϑ_n 0)` (`Dom.lean`) is the domained term for the intended value of `|ID_n|`. `EpsilonZero.lean` shows that `ϑ₀ 0` is the notation's own `ε₀`: it is the least fixed -point of the notation's `ω^·` (`isLeast_epsilonZero`) and the supremum of the ω-tower over `0` -(`lt_epsilonZero_iff`). Above the +`c n = ϑ₀(ϑ_n 0)` (`Dom.lean`) is the domained term for the intended value of `|ID_n|`. +`EpsilonZero.lean` shows that `ϑ₀ 0` is the least fixed point of the notation's `ω^·` +(`isLeast_epsilonZero`) and the supremum of the ω-tower over `0` (`lt_epsilonZero_iff`). Above the raw system, `HullSingle.lean` proves the level-free hull operator is least (`theta_isLeastS`, Wilken's Proposition 3.9 at every level at once), and `HullDom.lean` derives the domain lemma the collapsing theorem needs from it (`dom_add_omegaPow`) while also recording where the audited