Review the spectral literature package statement by statement (lot 2) - #164
Open
gift-framework wants to merge 1 commit into
Open
Review the spectral literature package statement by statement (lot 2)#164gift-framework wants to merge 1 commit into
gift-framework wants to merge 1 commit into
Conversation
…(lot 2) Drop the dead torsion_free_correction field of LiteraturePackage: nothing projected it and the public theorem of that name is proved without the package, so the literature_package axiom becomes strictly weaker. Document the two remaining fields by their exact Lean types (they constrain the mass gap only). Mark the two spectral attributions UNVERIFIED: the cited CGN title and DOI placeholder were not found (the published CGN papers are arXiv:1505.02734 and Ann. Glob. Anal. Geom. 2023), and the Langlais reference resolves to arXiv:2301.03513, not a journal article. Replace the five native_decide occurrences of this file (rational arithmetic on 14/99) by norm_num after rewriting with dim_G2_eq and H_star_eq (1481 -> 1476). Axiom count unchanged at 14. Local check on Lean 4.33.1: lake build (8855 jobs), lake build Verification (8859 jobs, 3764 theorems audited, no unapproved axiom), blueprint sync, regenerated proof inventory. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XFcYxvCfZYUqw3bjZ6fnRd
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.
Summary
Lot 2 of the modernization follow-up, derived from
docs/proof-guide.md(Remaining mathematical work).torsion_free_correctionfield ofLiteraturePackage: nothing projected it and the public theorem of that name is proved without the package, so theliterature_packageaxiom becomes strictly weaker. Axiom count unchanged (14).10.1007/s00222-024-XXXXXwere not found; the published CGN papers are arXiv:1505.02734 and Ann. Glob. Anal. Geom. 2023 (10.1007/s10455-023-09893-1). The Langlais reference resolves to arXiv:2301.03513, not a journal article. No mathematical content changed.native_decideoccurrences of this file (rational arithmetic on 14/99) byrw [dim_G2_eq, H_star_eq]; norm_num(1481 -> 1476).docs/proof-inventory.json; record the lot indocs/modernization.mdanddocs/proof-guide.md.Validation (local, Lean 4.33.1 / Mathlib 0df444a3)
lake build: 8855 jobs, success.lake build Verification: 8859 jobs, 3764 library theorems audited, 1448 depend on native evaluation, no unapproved axiom.scripts/check_blueprint_sync.sh: PASSED.scripts/proof_inventory.py --check: 14 axiom declarations, 0 holes, 1476native_decide.Checklist
🤖 Generated with Claude Code
https://claude.ai/code/session_01XFcYxvCfZYUqw3bjZ6fnRd