Modernize Lean and clarify the scope of the formal results - #162
Merged
Conversation
…nearity - HodgeTheory: `def b` -> `abbrev b` so `Fin (b k)` unfolds at instance transparency; restores `Decidable (i = j)` in K7_analysis_data and lets the original lambdas stand (the type annotations are no longer needed). - HodgeStarR7: star3_linear / star4_linear proved by `show` on the explicit coefficient form + `ring`, avoiding `simp` on a goal that 4.33 rejects at implicit transparency (Fin (Nat.choose 7 4) vs Fin 35). lake build: 8855 jobs, no errors, no sorry. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WSJVBCnUZ6DQoYqp1CFt8Q
`let mut count := 0` was inferred as MessageData from its later use inside
`m!"…{count}…"` on Lean 4.33, breaking `count + 1`. Explicit `: Nat`.
lake build && lake build Verification: 8859 jobs, audit OK
(3765 library theorems, no unapproved axiom).
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WSJVBCnUZ6DQoYqp1CFt8Q
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.
The presentation conflated numerical index conditions with analytic embedding theorems and a constant form model with compact G₂ existence. This change gives those results precise names, retains compatibility aliases and documents the actual assumptions.
Validation: source scanner regression tests, version consistency and blueprint synchronization pass locally. The first migration Actions run compiled both imported analysis proofs and identified import-order and Mathlib compatibility failures. Commit 8bfd846 addresses them; the next build is running. Local Lean cannot initialize in the Work runtime, so Actions is the compilation gate. Keep this PR in draft until the full build and audit pass.
See docs/modernization.md for evidence and remaining obligations. No project axiom is claimed discharged and no completed compact G₂ construction is claimed.