Repository navigation
ε₀ on ThetaNote and ThetaWNoteD: least fixed point of ω^· and supremum of the ω-tower - #2
Open
timbrigham wants to merge 3 commits into
Open
timbrigham wants to merge 3 commits into
timbrigham wants to merge 3 commits into
Conversation
… 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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FJrffXdNS9Weh7DwnUt9PV
…e 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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FJrffXdNS9Weh7DwnUt9PV
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FJrffXdNS9Weh7DwnUt9PV
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two small modules, one per ϑ-notation, stating that
ϑ 0(onThetaNote) andϑ₀ 0(onThetaWNoteD) are the least fixed point of the notation's ownomegaPowand the supremum of the ω-tower over0. Fulllake buildandscripts/AxiomCheck.leanpass on top of 53db882. Feel free to rename, move, or close.New declarations, in
Ordinal/Theta/EpsilonZero.leanandOrdinal/ThetaW/EpsilonZero.lean(namespacesThetaNote/ThetaWNoteD):isLeast_epsilonZero : IsLeast {a | omegaPow a = a} epsilonZerolt_epsilonZero_iff : a < epsilonZero ↔ ∃ m, a < omegaTower m zero(reusesomegaTowerfromHullCofinal.lean)omegaPow_epsilonZero,epsilonZero_le_of_omegaPow_eq,omegaPow_ne_self_of_lt_epsilonZero,omegaTower_zero_lt_epsilonZero,exists_lt_omegaTower_of_lt_epsilonZeroHow. Leastness rests on a raw-term lemma,
ThetaTerm.theta_zero_le_of_ofList_eq/ThetaWTerm.theta_zero_zero_le_of_ofList_eq: ifofList [t] = tthenϑ 0 ≤ t, with no normal-form or domain hypothesis. It is a case split ontusing the existing order clauses (theta_lt_Omega(_iff),theta_lt_theta_of_lt,theta_lt_theta_of_lt_level), and does not use well-foundedness. The supremum is by induction on term length: a notation belowϑ 0is not principal, so it is a Cantor sum whose entries are each below some tower stage (lt_prin_iff,lt_omegaPow_iff).Other changes: two import lines in
OrdinalAnalysis.lean, six#guard_msgsentries inscripts/AxiomCheck.lean, and a mention of each file in the README. The four bundled theorems print[propext, Classical.choice, Quot.sound]. The two raw-term lemmas print[propext, Quot.sound], and their#guard_msgsentries fix that axiom set.Also checked: the six declarations pinned in
AxiomCheck.leanpass nanoda on a lean4export (v4.33.0) export of those names, with the two raw-term lemmas checked withClassical.choiceleft out ofpermitted_axioms.I didn't find a declaration that names the ε₀ term on either ϑ-notation or states either property, but I may have missed one.
Claude wrote this PR (the proofs and this description) at my direction. — Tim