Repository navigation
Conversation
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
`gentzen_theorem` is stated about the coded ordering `≺` and read as
`|PA| = ε₀`, but nothing in the repo said `≺` has order type ε₀. New
`Gentzen/OrderType.lean` says it, sorry-free:
precF_type_eq_epsilon0 : Ordinal.type precF = ε₀
where `precF` is `PrecStandard.precN` restricted to its field
`{n : ℕ // isNF n}`. `CodeSurj.isNF_iff_exists_nonote` gives
surjectivity of `nonoteCode` onto the field and `precN_code_iff` gives
both order-preservation and (via trichotomy) injectivity, so `codeIso`
is an order iso `(NONote, <) ≃r (Field, precF)`. The missing input,
`Set.range NONote.repr = Set.Iio ε₀`, is not in mathlib and is proved
here (adapted from gotrevor/goodstein-independence, Apache 2.0),
yielding `reprIso : NONote ≃o Set.Iio ε₀` and `typeLT NONote = ε₀`.
Also `precF_iff_eval_precCode`, pinning `precF` to the literal
`precAt precCode` spelling `gentzen_theorem` uses, and the corollary
`gentzen_theorem_with_order_type`. Two AxiomCheck pins added.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FZErZDHWi4xH8Rfx3ADVaX
Owner
Author
|
Upstream MaxWellApexLab#1 was closed. |
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.
[ Claude wrote this PR, the proof and this description, at my direction. ]
gentzen_theoremconcludes |PA| = ε₀ in its docstring, but nothing in the repo states that≺has order type ε₀; that reading rests onprecN_code_iffplus mathlib'sNONote. This addsGentzen/OrderType.lean, which makes it a theorem:where
precFisPrecStandard.precNon its field{n : ℕ // isNF n}. Alsogentzen_theorem_with_order_type(the conjunction), andprecF_iff_eval_precCode, which tiesprecFto the exactprecCodespelling ingentzen_theorem.Route:
nonoteCodeis an order isoNONote ≃ field(fromprecN_code_iffandisNF_iff_exists_nonote), andNONote.repris an order iso ontoIio ε₀. The surjectivity half isn't in mathlib; it's adapted from goodstein-independence (credited in the file header). New file plus one import line plus AxiomCheck pins;lake buildgreen on 87baec7.Happy to adjust names or placement to your taste.
Our goodstein-independence repo proves Goodstein / Hydra / Paris-Harrington independence on mathlib's
ONotetoo, and yourInternalONotelooks like it shares ancestry with a wip file of ours, so there may be more to connect.