Connect 6 orphaned modules to main dependency graph #88
Conversation
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
Adds abbrevs to Certificate.lean for previously disconnected modules: **V3.0 Analytical modules (DifferentialForms, ImplicitFunction):** - v3_hodge_duality, v3_omega2_decomposition, v3_omega3_decomposition - v3_k7_betti_numbers, v3_poincare_duality - v3_ift_conditions (implicit function theorem) **V1.5-V1.7 Relations modules:** - v15_exceptional_groups (5 relations: alpha_s^2, F4, delta_penta, etc.) - v15_base_decomposition (6 relations) - v15_extended_decomposition (10 relations) - v16_mass_factorization (3477, Von Staudt, T_61, Triade) - v17_exceptional_chain (tau_num, E7, E6, E8 chain) These modules were imported but had no abbrev edges connecting them to the Certificate dependency graph, causing isolated clusters in the blueprint visualization.
Convert axioms to theorems using Mathlib bounds: - exp_one_gt: 2.7 < e via Taylor series lower bound - exp_one_lt: e < 2.72 via log comparison with 3 This is a test commit - CI will verify if the proofs work. If they fail, we may need stronger Mathlib lemmas or interval arithmetic.
The attempted proofs failed because: - Real.add_one_lt_exp only gives 2 < e (not 2.7 < e) - Real.one_lt_log_iff doesn't exist in this Mathlib version - Tight bounds on e require Taylor series with remainder or interval arithmetic These bounds remain as axioms with clear numerical justification: - e = 2.718281828... (well-established mathematical constant) - 2.7 < e < 2.72 is trivially verified numerically Future work: implement proper interval arithmetic for transcendental bounds.
Replace the E8_basis axiom with explicit definitions of the 8 simple roots: - α₁ through α₆: integer vectors (differences of standard basis) - α₇: e₆ + e₇ (D-type connection) - α₈: half-integer vector (-1/2,-1/2,-1/2,-1/2,-1/2,1/2,1/2,-1/2) Added: - mkR8: helper to construct R8 vectors - E8_α1 through E8_α8: individual simple root definitions - E8_basis: explicit definition (no longer axiom!) - E8_α1_in_lattice: proof that α₁ is in E8 lattice - E8_α8_in_lattice: proof that α₈ is in E8 lattice E8_basis_generates remains an axiom (proving generation requires significant linear algebra infrastructure). This is progress toward a potential Mathlib contribution for E8 formalization.
- Mark all E8 basis definitions as noncomputable (required for ℝ division) - Remove failing membership proofs (E8_α1_in_lattice, E8_α8_in_lattice) - Keep explicit E8 simple root definitions - E8_basis_generates remains axiom (proving generation is non-trivial) The 8 simple roots are now explicitly defined as noncomputable defs, which is progress over having E8_basis itself as an axiom.
## Changes - CHANGELOG.md: Document v3.1.11 features - README.md: Bump version footer - _version.py: Bump to 3.1.11 - CLAUDE.md: Add lessons learned (§9-11) ## Summary - Connected 7 orphaned module clusters to blueprint - E8_basis converted from axiom to explicit definition - Axiom count: 41 (was 42) ## New CLAUDE.md Lessons - §9: Blueprint dependency graph orphans - §10: Explicit EuclideanSpace vectors (noncomputable) - §11: Numerical bounds on transcendentals (axioms)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Adds abbrevs to Certificate.lean for previously disconnected modules:
V3.0 Analytical modules (DifferentialForms, ImplicitFunction):
V1.5-V1.7 Relations modules:
These modules were imported but had no abbrev edges connecting them to the Certificate dependency graph, causing isolated clusters in the blueprint visualization.