v3.3.19: Remove 8 ad-hoc spectral gap axioms#145
Merged
gift-framework merged 1 commit intomainfrom Feb 13, 2026
Merged
Conversation
Remove Category E axioms that claimed specific values for the K₇ spectral gap (λ₁ = 14/99 or 13/99). These predictions were circular and not independently verifiable. The spectral gap is now treated as an open research question. Axioms removed: - universal_spectral_law, K7_spectral_law, K7_mass_gap_is_14_over_99 - K7_physical_spectral_law, K7_physical_mass_gap (UniversalLaw.lean) - K7_cheeger_constant (CheegerInequality.lean) - GIFT_mass_gap_relation (YangMills.lean) - canonical_neck_length_conjecture (LiteratureAxioms.lean) Preserved intact: - MassGapRatio.lean (pure algebra, zero axioms) - PhysicalSpectralGap.lean (axiom-free derivation of 13/99) - All proven ℚ theorems (coprimality, bounds, certificates) Full build: 2641 jobs, zero errors. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
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
Axioms removed
UniversalLaw.leanuniversal_spectral_lawUniversalLaw.leanK7_spectral_lawUniversalLaw.leanK7_mass_gap_is_14_over_99UniversalLaw.leanK7_physical_spectral_lawUniversalLaw.leanK7_physical_mass_gapCheegerInequality.leanK7_cheeger_constantYangMills.leanGIFT_mass_gap_relationLiteratureAxioms.leancanonical_neck_length_conjectureMotivation
Numerical investigation (graph Laplacian on TCS-sampled K₇) showed the spectral gap cannot be reliably determined — values range from 12.7 to 20.7 depending on bandwidth parameter k. The 14/99 prediction was circular in Lean (axiom → theorem using axiom). Removing these gives more intellectual honesty.
Preserved intact
MassGapRatio.lean— Pure ℚ algebra (zero axioms)PhysicalSpectralGap.lean— Axiom-free: IF λ₁×H* = dim(G₂)−h THEN 13/99Test plan
lake buildpasses (2641 jobs)🤖 Generated with Claude Code