A Lean 4 + Mathlib formalization of spectral triples from Alain Connes' noncommutative geometry: odd and even (Z₂-graded) spectral triples, the resolvent of the Dirac operator, and finitely-summable triples — working toward the Fredholm index pairing.
📐 Blueprint · 🗺️ Design notes · 📋 Implementation plan & status
All source is sorry-free and axiom-free. Built against Mathlib v4.30.0.
| File | Contents |
|---|---|
SpectralTriples/Basic.lean |
IsOddSpectralTriple, IsEvenSpectralTriple (Dirac operator D as an unbounded LinearPMap) and their basic API |
SpectralTriples/Resolvent.lean |
LinearPMap.resolventSet / resolvent (adapted from Mathlib PR #29624, Moritz Doll) |
SpectralTriples/FinitelySummable.lean |
self-adjoint resolvent estimates and IsFinitelySummableSpectralTriple (compact resolvent) |
SpectralTriples/Index.lean |
the graded-kernel index of an even triple, with finiteDimensional_Dkernel (compact resolvent ⇒ ker D finite-dim, so D⁺ is Fredholm) |
SpectralTriples/DiagonalOperator.lean |
block-diagonal operators on ℓ² and the compactness criterion isCompactOperator_diagL (block norms → 0 ⇒ compact) |
SpectralTriples/Examples/Torus.lean |
the 2-torus T² Dirac triple: self-adjoint D, compact resolvent at i, grading γ = σ₃, the shift representation of ℂ[ℤ²], assembled as an even, finitely-summable spectral triple |
The encoding decision: the unbounded LinearPMap picture is the spine, with a
bounded Fredholm-module layer planned at Phase 2 for the index pairing. See
PLAN.md for the rationale, the immediate next step, and the phase
outline; DESIGN.md for the full
mathematical vision and worked examples.
lake exe cache get # fetch prebuilt Mathlib
lake buildConnes, Noncommutative Geometry (1994); Gracia-Bondía–Várilly–Figueroa,
Elements of Noncommutative Geometry (2001); Higson–Roe, Analytic
K-Homology (2000). Reference notes live in
SpectralTriples/refs/.
This project follows a lightweight assurance convention — verification /
validation / faithfulness, axiom vetting, and a standardized formalization.yaml
project card. Local settings:
| Setting | Where |
|---|---|
| Project card | formalization.yaml |
| Faithfulness map (informal ↔ formal) | audit/FAITHFULNESS.md |
| Kernel axiom certificate (generated, CI-diffed) | audit/axiom-report.txt |
| Axiom audit | AXIOM_AUDIT.md — 0 project axioms |
| Vetting strictness | audit/vetting/policy.yml — L1 |
All tracked headlines are sorry-free and axiom-clean (standard-three only:
propext, Classical.choice, Quot.sound); CI regenerates audit/axiom-report.txt
from #print axioms and fails on drift. Regenerate locally with:
lake env lean scripts/axiom_report.lean > audit/axiom-report.txtJon Bannon, Michael R. Douglas. Released under the Apache 2.0 license.