From f996df0b7488a6cb9d88608d579b328a8f71f24b Mon Sep 17 00:00:00 2001 From: Brieuc Date: Wed, 9 Sep 2026 14:44:23 +0200 Subject: [PATCH] proof: review the spectral literature package statement by statement (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 Claude-Session: https://claude.ai/code/session_01XFcYxvCfZYUqw3bjZ6fnRd --- GIFT/Spectral/LiteratureAxioms.lean | 92 ++++++++++++++++++----------- docs/modernization.md | 12 ++++ docs/proof-guide.md | 21 ++++--- docs/proof-inventory.json | 22 +------ 4 files changed, 83 insertions(+), 64 deletions(-) diff --git a/GIFT/Spectral/LiteratureAxioms.lean b/GIFT/Spectral/LiteratureAxioms.lean index b59ad7b..40dc8d3 100644 --- a/GIFT/Spectral/LiteratureAxioms.lean +++ b/GIFT/Spectral/LiteratureAxioms.lean @@ -9,16 +9,24 @@ formal content; names and citations do not strengthen those statements. ## Declaration Classification (v3.3.42) ### Historical provenance and current status -The two CGN declarations remain projections from an axiomatic package. The -historically Joyce-named declaration is now an elementary theorem with a much -weaker type than the cited geometric result. +The two CGN-attributed declarations remain projections from an axiomatic +package. The historically Joyce-named declaration is an elementary theorem with +a much weaker type than the cited geometric result; the package no longer +carries a field of that name (lot 2, 2026-09-09). + +What the Lean types say, independently of the names: +- `no_small_eigenvalues`: the mass gap `λ₁` of `K` is not in the open interval + `(0, gap_constant / L)`. It is a statement about the first eigenvalue only, + not about the absence of every eigenvalue in that interval. +- `cheeger_lower_bound`: `λ₁ ≥ cheeger_constant / L²`. +No field mentions a G₂ structure, a torsion-free correction or a Betti number. | Declaration | Paper | Journal | Year | Status | |-------|-------|---------|------|--------| | `cgn_no_small_eigenvalues` | Crowley-Goette-Nordström | Inventiones | 2024 | **FUSED** into `literature_package` | | `cgn_cheeger_lower_bound` | Crowley-Goette-Nordström | Inventiones | 2024 | **FUSED** into `literature_package` | -| `torsion_free_correction` | Historical Joyce attribution | — | — | **PROVED** from its current weak type | -| `literature_package` | CGN claims plus a legacy compatibility field | — | — | **AXIOM** | +| `torsion_free_correction` | Historical Joyce attribution | — | — | **PROVED** from its current weak type (no longer a package field) | +| `literature_package` | two CGN-attributed spectral claims | — | — | **AXIOM** | ## Key Results @@ -34,17 +42,28 @@ weaker type than the cited geometric result. ## Full References -- Langlais, P. (2024). "Spectral density of TCS manifolds" - Commun. Math. Phys., DOI: [pending] +Citation status (checked 2026-09-09, lot 2): the two spectral references below +could not be confirmed as written and are kept as historical attributions. -- Crowley, D., Goette, S., & Nordström, J. (2024). "The spectral geometry - of twisted connected sum G₂-manifolds" - Inventiones Mathematicae, DOI: 10.1007/s00222-024-XXXXX +- Langlais, T. "Analysis and spectral theory of neck-stretching problems", + arXiv:2301.03513 (the density-of-low-eigenvalues results for twisted + connected sums are stated there). The former entry "Langlais, P. (2024), + Commun. Math. Phys., Theorem 2.7, DOI pending" was not found as a + published article; theorem numbering UNVERIFIED. + +- Crowley, D., Goette, S., & Nordström, J. — the title "The spectral geometry + of twisted connected sum G₂-manifolds" (Inventiones, 2024) and the DOI + placeholder `10.1007/s00222-024-XXXXX` were not found. The published CGN + papers are "An analytic invariant of G₂ manifolds" (arXiv:1505.02734) and + "Extra-twisted connected sum G₂-manifolds" (Ann. Glob. Anal. Geom., 2023, + DOI 10.1007/s10455-023-09893-1); neither is a spectral-gap paper. + "Proposition 3.16" and "line 3598" are UNVERIFIED pointers. - Joyce, D.D. (2000). "Compact Manifolds with Special Holonomy" Oxford University Press, ISBN: 0-19-850601-5 -Version: 2.0.0 (v3.3.42: historical literature axiom consolidation 3 → 1) +Version: 2.1.0 (lot 2, 2026-09-09: legacy field dropped, types documented, +citations marked; v3.3.42: historical literature axiom consolidation 3 → 1) -/ import GIFT.Core @@ -136,12 +155,15 @@ theorem K3_S1_density_coeff_3 : density_coefficient_K3S1 3 = 88 := rfl /-- Bundled data for TCS spectral geometry. -The substantive literature-attributed fields are: -- CGN Proposition 3.16: no small eigenvalues -- CGN line 3598: Cheeger-based lower bound +The two literature-attributed fields are: +- "no small eigenvalues" (attributed to CGN Prop. 3.16, UNVERIFIED): the mass + gap is not in `(0, gap_constant / L)`; +- Cheeger-type lower bound (attributed to CGN, UNVERIFIED): `λ₁ ≥ C' / L²`. -The final field is retained for compatibility with the structure introduced in -v3.3.42. Its type does not state Joyce's torsion-free correction theorem. +The legacy field `torsion_free_correction` (type: two positive reals exist) +was dropped in lot 2 (2026-09-09): nothing projected it, and the public theorem +of that name is proved without the package. The axiom is therefore strictly +weaker than before. **References:** - Crowley, D., Goette, S., & Nordström, J. (2024). @@ -149,45 +171,44 @@ v3.3.42. Its type does not state Joyce's torsion-free correction theorem. - Joyce, D.D. (2000). "Compact Manifolds with Special Holonomy", Oxford UP. -/ structure LiteraturePackage (K : TCSManifold) where - /-- CGN Prop. 3.16: gap isolation constant -/ + /-- Gap isolation constant (attributed to CGN Prop. 3.16, UNVERIFIED) -/ gap_constant : ℝ /-- Gap constant is positive -/ gap_constant_pos : gap_constant > 0 - /-- No eigenvalues in (0, c/L) -/ + /-- The mass gap is not in (0, c/L). This is a statement about `MassGap` + only, not about every eigenvalue of the interval. -/ no_small_eigenvalues : ∀ (hyp : TCSHypotheses K), ∀ ev : ℝ, 0 < ev → ev < gap_constant / K.neckLength → MassGap K.toCompactManifold ≤ ev → False - /-- CGN line 3598: Cheeger lower bound constant -/ + /-- Cheeger-type lower bound constant (attributed to CGN, UNVERIFIED) -/ cheeger_constant : ℝ /-- Cheeger constant is positive -/ cheeger_constant_pos : cheeger_constant > 0 /-- C'/(ℓ+r)² ≤ λ₁ -/ cheeger_lower_bound : MassGap K.toCompactManifold ≥ cheeger_constant / K.neckLength ^ 2 - /-- Legacy compatibility field. Its type only asserts the existence of two - positive real numbers; the public theorem below no longer projects it. -/ - torsion_free_correction : ∀ (k : ℕ), ∃ C δ : ℝ, C > 0 ∧ δ > 0 /-- Literature results hold for any TCS manifold. -**(Literature axiom)** — Contains two literature-attributed spectral claims and -a legacy field with an elementary positivity type. +**(Literature axiom)** — Contains exactly two literature-attributed spectral +claims about the mass gap of a TCS manifold; nothing else. **Historical axiom consolidation (v3.3.42):** Replaced `cgn_no_small_eigenvalues`, `cgn_cheeger_lower_bound` and the former -`torsion_free_correction` axiom by one package. The last field now remains only -for structure compatibility; the public theorem of that name is elementary. -/ +`torsion_free_correction` axiom by one package. Lot 2 (2026-09-09) removed the +last, dead field; the public theorem of that name is elementary. -/ axiom literature_package (K : TCSManifold) : LiteraturePackage K -- ============================================================================ -- BACKWARD-COMPATIBLE DECLARATIONS -- ============================================================================ -/-- CGN Proposition 3.16: No small eigenvalues except 0. +/-- The mass gap is not in `(0, c/L)` for some `c > 0` (historical name +"no small eigenvalues"; the type constrains `MassGap` only). **Formerly axiom**, now structure projection from LiteraturePackage (v3.3.42). -**Citation:** Crowley, Goette, Nordström (2024), Inventiones Math., Prop. 3.16 -/ +**Attribution (UNVERIFIED):** Crowley, Goette, Nordström, "Prop. 3.16". -/ theorem cgn_no_small_eigenvalues (K : TCSManifold) (hyp : TCSHypotheses K) : ∃ c : ℝ, c > 0 ∧ ∀ ev : ℝ, 0 < ev → ev < c / K.neckLength → @@ -195,11 +216,11 @@ theorem cgn_no_small_eigenvalues (K : TCSManifold) (hyp : TCSHypotheses K) : let pkg := literature_package K ⟨pkg.gap_constant, pkg.gap_constant_pos, pkg.no_small_eigenvalues hyp⟩ -/-- Cheeger-based lower bound from CGN (line 3598). +/-- Cheeger-type lower bound `λ₁ ≥ C' / L²` for some `C' > 0`. **Formerly axiom**, now structure projection from LiteraturePackage (v3.3.42). -**Citation:** Crowley, Goette, Nordström (2024), Inventiones Math., line 3598 -/ +**Attribution (UNVERIFIED):** Crowley, Goette, Nordström, "line 3598". -/ theorem cgn_cheeger_lower_bound (K : TCSManifold) : ∃ C' : ℝ, C' > 0 ∧ MassGap K.toCompactManifold ≥ C' / K.neckLength ^ 2 := @@ -241,13 +262,12 @@ Then: -/ theorem gift_prediction_structure : (14 : ℚ) / 99 = dim_G2 / H_star := by - simp only [dim_G2, H_star] - native_decide + rw [GIFT.Algebraic.G2.dim_G2_eq, GIFT.Algebraic.BettiNumbers.H_star_eq]; norm_num /-- The prediction 14/99 is consistent with TCS bounds structure -/ theorem gift_prediction_in_range : (1 : ℚ) / 100 < 14 / 99 ∧ (14 : ℚ) / 99 < 1 / 4 := by - native_decide + norm_num -- ============================================================================ -- CERTIFICATE @@ -266,8 +286,8 @@ theorem literature_axioms_certificate : (1 : ℚ) / 100 < 14 / 99 ∧ (14 : ℚ) / 99 < 1 / 4 := by refine ⟨rfl, rfl, rfl, ?_, ?_, ?_⟩ - · simp only [dim_G2, H_star]; native_decide - · native_decide - · native_decide + · rw [GIFT.Algebraic.G2.dim_G2_eq, GIFT.Algebraic.BettiNumbers.H_star_eq]; norm_num + · norm_num + · norm_num end GIFT.Spectral.LiteratureAxioms diff --git a/docs/modernization.md b/docs/modernization.md index 14075ce..2269aa7 100644 --- a/docs/modernization.md +++ b/docs/modernization.md @@ -78,6 +78,18 @@ a precise mathematical review. The new cube estimate is not the dimension-seven H⁴ embedding theorem. Historical constants, release tags and Koide comparison inputs are unchanged. This branch does not claim a completed compact G₂ construction. +## Follow-up lots + +Lot 2 (2026-09-09, branch `claude/k7-lot-2-literature-package`): statement-by-statement +review of `GIFT/Spectral/LiteratureAxioms.lean`. The dead `torsion_free_correction` +field of `LiteraturePackage` was removed (nothing projected it), so the axiom +`literature_package` is strictly weaker; the two remaining fields are documented by +their exact types (mass gap only); the two spectral citations could not be confirmed +and are marked UNVERIFIED in the source; the five `native_decide` occurrences of the +file (rational arithmetic on `14/99`) were replaced by `norm_num` (1481 → 1476). +Axiom count unchanged at 14. Local check: `lake build`, `lake build Verification`, +blueprint synchronization and the generated inventory. + ## Migration build history [Run 34105836451](https://github.com/Arithmon/K7-Lean/actions/runs/34105836451) diff --git a/docs/proof-guide.md b/docs/proof-guide.md index 4276b06..891f1fd 100644 --- a/docs/proof-guide.md +++ b/docs/proof-guide.md @@ -59,13 +59,20 @@ quantities and proofs relating exact enclosures to those definitions. Checking an integer aggregate of externally supplied endpoints does not prove that the endpoints enclose the intended geometric quantity. -The spectral literature package needs a statement-by-statement review. Its legacy -`torsion_free_correction` field only asserts the existence of two positive real -numbers; the public theorem of that name now proves this elementary statement -without using the package. Neither declaration formalizes Joyce's correction -theorem. The historical citation contains a placeholder DOI. The source's `K3_S1` -Betti table is also not a proof of the cohomology of a product. These items must -not be advertised as a formalization of the cited geometric results. +The spectral literature package was reviewed statement by statement on +2026-09-09 (lot 2). Its legacy `torsion_free_correction` field was removed: nothing +projected it, and the public theorem of that name proves its elementary statement +without the package, so the axiom `literature_package` is now strictly weaker. The +two remaining fields constrain the mass gap only (`λ₁ ∉ (0, c/L)` and +`λ₁ ≥ C'/L²`); their docstrings now say exactly that. Their attributions could not +be confirmed: the cited CGN title and DOI placeholder were not found, and the +Langlais reference resolves to arXiv:2301.03513 rather than a journal article. Both +are marked UNVERIFIED in the source. Neither declaration formalizes Joyce's +correction theorem, and the `K3_S1` Betti table is data, not a proof of the +cohomology of a product. These items must not be advertised as a formalization of +the cited geometric results. The mathematical review of the two claims themselves +(is the statement in the literature, with which constants and hypotheses) is still +open. The Chebyshev U completeness lemma from FLT has not been imported: no current result here requires it. A Chebyshev–Cholesky error estimate needs approximation diff --git a/docs/proof-inventory.json b/docs/proof-inventory.json index 25ae9ae..2202470 100644 --- a/docs/proof-inventory.json +++ b/docs/proof-inventory.json @@ -58,7 +58,7 @@ }, { "file": "GIFT/Spectral/LiteratureAxioms.lean", - "line": 180, + "line": 200, "name": "literature_package" }, { @@ -5533,26 +5533,6 @@ "file": "GIFT/Spectral/KKSpectralBridge.lean", "line": 253 }, - { - "file": "GIFT/Spectral/LiteratureAxioms.lean", - "line": 245 - }, - { - "file": "GIFT/Spectral/LiteratureAxioms.lean", - "line": 250 - }, - { - "file": "GIFT/Spectral/LiteratureAxioms.lean", - "line": 269 - }, - { - "file": "GIFT/Spectral/LiteratureAxioms.lean", - "line": 270 - }, - { - "file": "GIFT/Spectral/LiteratureAxioms.lean", - "line": 271 - }, { "file": "GIFT/Spectral/MassGapRatio.lean", "line": 85