diff --git a/SpectralTriples/CompactOperators.lean b/SpectralTriples/CompactOperators.lean
index 1636a9d..9ba5ab3 100644
--- a/SpectralTriples/CompactOperators.lean
+++ b/SpectralTriples/CompactOperators.lean
@@ -16,9 +16,10 @@ public import Mathlib.Analysis.InnerProductSpace.Spectrum
 
 This file proves, for an inner product space `H`, that `1 - K` is a Fredholm linear map
 (`SpectralTriples.Fredholm.IsFredholm`) whenever `K` is a compact operator on `H`. This is the
-Hilbert-space case of the classical Riesz–Schauder theorem; it is not yet in Mathlib (only the
-weaker spectral dichotomy `IsCompactOperator.hasEigenvalue_or_mem_resolventSet` is), so we prove
-it here from scratch.
+structural part of the Hilbert-space case of the classical Riesz–Schauder theorem (finite
+kernel, closed range, finite-dimensional cokernel); the further classical fact that the index
+is `0` is not proved here. None of this is yet in Mathlib (only the weaker spectral dichotomy
+`IsCompactOperator.hasEigenvalue_or_mem_resolventSet` is), so we prove it here from scratch.
 
 ## Main results
 
@@ -185,6 +186,32 @@ theorem adjoint {K : H →L[𝕜] H} (hK : IsCompactOperator K) :
 
 end IsCompactOperator
 
+namespace Submodule
+
+/-- For a submodule of a Hilbert space with an orthogonal projection (e.g. one with closed
+range), the quotient by it is linearly equivalent to its orthogonal complement. -/
+noncomputable def quotientEquivOrthogonal (K : Submodule 𝕜 H) [K.HasOrthogonalProjection] :
+    (H ⧸ K) ≃ₗ[𝕜] Kᗮ :=
+  Submodule.quotientEquivOfIsCompl K Kᗮ Submodule.isCompl_orthogonal_of_hasOrthogonalProjection
+
+omit [CompleteSpace H] in
+/-- The quotient by a submodule with an orthogonal projection has the same finite dimension as
+its orthogonal complement. -/
+theorem finrank_quotient_eq_finrank_orthogonal (K : Submodule 𝕜 H) [K.HasOrthogonalProjection] :
+    Module.finrank 𝕜 (H ⧸ K) = Module.finrank 𝕜 Kᗮ :=
+  (K.quotientEquivOrthogonal).finrank_eq
+
+omit [CompleteSpace H] in
+/-- The quotient by a submodule with an orthogonal projection is finite-dimensional whenever
+its orthogonal complement is. -/
+theorem finiteDimensional_quotient_of_finiteDimensional_orthogonal (K : Submodule 𝕜 H)
+    [K.HasOrthogonalProjection] [FiniteDimensional 𝕜 Kᗮ] :
+    FiniteDimensional 𝕜 (H ⧸ K) :=
+  FiniteDimensional.of_injective (K.quotientEquivOrthogonal).toLinearMap
+    (K.quotientEquivOrthogonal).injective
+
+end Submodule
+
 namespace SpectralTriples.Fredholm
 
 /-- **Fredholm-ness of compact perturbations of the identity** (the structural part of the
@@ -344,10 +371,8 @@ theorem isFredholm_one_sub {K : H →L[𝕜] H} (hK : IsCompactOperator K) :
     exact (ContinuousLinearMap.adjoint K).finite_dimensional_eigenspace hKadj 1 one_ne_zero
   haveI hcokerfd : FiniteDimensional 𝕜 (LinearMap.range T.toLinearMap)ᗮ := by
     rw [T.orthogonal_range]; exact hNadjfd
-  have hequiv := Submodule.quotientEquivOfIsCompl (LinearMap.range T.toLinearMap)
-    (LinearMap.range T.toLinearMap)ᗮ Submodule.isCompl_orthogonal_of_hasOrthogonalProjection
   haveI : FiniteDimensional 𝕜 (H ⧸ LinearMap.range T.toLinearMap) :=
-    FiniteDimensional.of_injective hequiv.toLinearMap hequiv.injective
+    (LinearMap.range T.toLinearMap).finiteDimensional_quotient_of_finiteDimensional_orthogonal
   exact ⟨hNfd, hclosed_T, ‹FiniteDimensional 𝕜 (H ⧸ LinearMap.range T.toLinearMap)›⟩
 
 end SpectralTriples.Fredholm
diff --git a/SpectralTriples/DiagonalOperator.lean b/SpectralTriples/DiagonalOperator.lean
index a1da530..9b44c68 100644
--- a/SpectralTriples/DiagonalOperator.lean
+++ b/SpectralTriples/DiagonalOperator.lean
@@ -8,6 +8,7 @@ module
 
 public import Mathlib.Analysis.InnerProductSpace.l2Space
 public import Mathlib.Analysis.Normed.Operator.Compact.Basic
+public import Mathlib.Analysis.InnerProductSpace.LinearPMap
 
 /-! # Block-diagonal operators on `ℓ²`
 
@@ -40,7 +41,7 @@ exactly such block-diagonal operators with block norms `→ 0`.
 namespace lpDiag
 
 open scoped Topology
-open Filter
+open Filter LinearPMap
 
 variable {α 𝕜 : Type*} [RCLike 𝕜] {G : α → Type*}
     [∀ i, NormedAddCommGroup (G i)] [∀ i, InnerProductSpace 𝕜 (G i)]
@@ -217,4 +218,144 @@ theorem isCompactOperator_diagL (T : ∀ i, G i →L[𝕜] G i) {C : ℝ} (hC0 :
     exact tendsto_one_div_add_atTop_nhds_zero_nat
   exact isCompactOperator_of_tendsto htends (Filter.Eventually.of_forall hcompact)
 
+/-! ### The unbounded block-diagonal Dirac operator
+
+Given a family of *symmetric* (Hermitian) blocks `B i : G i →ₗ[𝕜] G i`, this section builds the
+associated unbounded "diagonal Dirac operator" on its maximal domain in `ℓ²(α; G)`, and proves
+it is self-adjoint. This is the analytic core shared by the `S¹` and `T²` Dirac examples: the
+circle's scalar multiplication by `n` and the torus's `2×2` spinor blocks are both instances of
+a symmetric block family, differing only in the fibre `G i` and the block `B i`. -/
+
+variable [∀ i, CompleteSpace (G i)]
+
+/-- The maximal domain of the unbounded block-diagonal operator with blocks `B`: those `a` for
+which `i ↦ B i (aᵢ)` is again square-summable. -/
+def diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) : Submodule 𝕜 (lp G 2) where
+  carrier := {a | Memℓp (fun i => B i (a i)) 2}
+  zero_mem' := by
+    have hzero : (fun i => B i ((0 : lp G 2) i)) = 0 := by
+      funext i; simp only [lp.coeFn_zero, Pi.zero_apply, _root_.map_zero]
+    simp only [Set.mem_setOf_eq, hzero]; exact zero_memℓp
+  add_mem' := fun {a b} ha hb => by
+    have heq : (fun i => B i ((a + b) i)) = (fun i => B i (a i)) + fun i => B i (b i) := by
+      funext i; simp only [lp.coeFn_add, Pi.add_apply, _root_.map_add]
+    rw [Set.mem_setOf_eq, heq]; exact ha.add hb
+  smul_mem' := fun c a ha => by
+    have heq : (fun i => B i ((c • a) i)) = c • fun i => B i (a i) := by
+      funext i; simp only [lp.coeFn_smul, Pi.smul_apply, _root_.map_smul]
+    rw [Set.mem_setOf_eq, heq]; exact ha.const_smul c
+
+omit [∀ i, CompleteSpace (G i)] in
+theorem mem_diracDomain_iff (B : ∀ i, G i →ₗ[𝕜] G i) (a : lp G 2) :
+    a ∈ diracDomain B ↔ Memℓp (fun i => B i (a i)) 2 := Iff.rfl
+
+/-- Coordinatewise application of the blocks, as an element of `ℓ²(α; G)`, given a proof the
+result is square-summable. -/
+noncomputable def applyDirac (B : ∀ i, G i →ₗ[𝕜] G i) (a : lp G 2)
+    (h : Memℓp (fun i => B i (a i)) 2) : lp G 2 :=
+  ⟨fun i => B i (a i), h⟩
+
+omit [∀ i, CompleteSpace (G i)] in
+@[simp] theorem coe_applyDirac (B : ∀ i, G i →ₗ[𝕜] G i) (a : lp G 2) (h) (i : α) :
+    (applyDirac B a h) i = B i (a i) := rfl
+
+/-- The unbounded block-diagonal operator on `ℓ²(α; G)` with blocks `B`, on its maximal domain
+`diracDomain B`. -/
+noncomputable def diracDirac (B : ∀ i, G i →ₗ[𝕜] G i) : lp G 2 →ₗ.[𝕜] lp G 2 where
+  domain := diracDomain B
+  toFun :=
+    { toFun := fun a => applyDirac B (a : lp G 2) ((mem_diracDomain_iff B _).mp a.2)
+      map_add' := fun a b => by
+        refine lp.ext (funext fun i => ?_)
+        simp only [coe_applyDirac, Submodule.coe_add, lp.coeFn_add, Pi.add_apply,
+          _root_.map_add]
+      map_smul' := fun c a => by
+        refine lp.ext (funext fun i => ?_)
+        simp only [coe_applyDirac, Submodule.coe_smul, lp.coeFn_smul, Pi.smul_apply,
+          _root_.map_smul, RingHom.id_apply] }
+
+omit [∀ i, CompleteSpace (G i)] in
+@[simp] theorem diracDirac_apply (B : ∀ i, G i →ₗ[𝕜] G i) (a : diracDomain B) (i : α) :
+    (diracDirac B a) i = B i ((a : lp G 2) i) := rfl
+
+omit [∀ i, CompleteSpace (G i)] in
+/-- The block-diagonal operator is symmetric (formally self-adjoint) when each block is. -/
+theorem diracDirac_isFormalAdjoint (B : ∀ i, G i →ₗ[𝕜] G i) (hB : ∀ i, (B i).IsSymmetric) :
+    (diracDirac B).IsFormalAdjoint (diracDirac B) := by
+  intro x y
+  rw [lp.inner_eq_tsum, lp.inner_eq_tsum]
+  refine tsum_congr fun i => ?_
+  rw [diracDirac_apply, diracDirac_apply]
+  exact hB i _ _
+
+omit [∀ i, CompleteSpace (G i)] in
+/-- Each single-mode vector lies in the maximal domain. -/
+theorem single_mem_diracDomain [DecidableEq α] (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) :
+    (lp.single 2 i v : lp G 2) ∈ diracDomain B := by
+  rw [mem_diracDomain_iff]
+  have hfun : (fun q => B q ((lp.single 2 i v : lp G 2) q))
+      = ⇑(lp.single 2 i (B i v) : lp G 2) := by
+    funext q
+    rcases eq_or_ne q i with h | h
+    · subst h; simp [lp.single_apply]
+    · simp [lp.single_apply, h, _root_.map_zero]
+  rw [hfun]
+  exact lp.memℓp _
+
+omit [∀ i, CompleteSpace (G i)] in
+/-- The image of a single-mode vector under the diagonal operator. -/
+theorem diracDirac_single [DecidableEq α] (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) :
+    diracDirac B ⟨lp.single 2 i v, single_mem_diracDomain B i v⟩
+      = (lp.single 2 i (B i v) : lp G 2) := by
+  refine lp.ext (funext fun q => ?_)
+  rcases eq_or_ne q i with h | h
+  · subst h; simp [diracDirac_apply, lp.single_apply]
+  · simp [diracDirac_apply, lp.single_apply, h, _root_.map_zero]
+
+/-- The maximal domain is dense: it contains every single-mode vector. -/
+theorem dense_diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) :
+    Dense ((diracDirac B).domain : Set (lp G 2)) := by
+  classical
+  change Dense (diracDomain B : Set (lp G 2))
+  have horth : (diracDomain B : Submodule 𝕜 (lp G 2))ᗮ = ⊥ := by
+    rw [Submodule.eq_bot_iff]
+    intro y hy
+    refine lp.ext (funext fun i => ?_)
+    refine ext_inner_left 𝕜 fun v => ?_
+    have h0 : inner 𝕜 (lp.single 2 i v : lp G 2) y = 0 := hy _ (single_mem_diracDomain B i v)
+    rw [lp.inner_single_left] at h0
+    rw [h0, lp.coeFn_zero, Pi.zero_apply, inner_zero_right]
+  have htop : (diracDomain B).topologicalClosure = ⊤ :=
+    (Submodule.topologicalClosure_eq_top_iff (K := diracDomain B)).mpr horth
+  rw [dense_iff_closure_eq, ← Submodule.topologicalClosure_coe, htop, Submodule.top_coe]
+
+/-- The block-diagonal operator with symmetric blocks is contained in its adjoint. -/
+theorem diracDirac_le_adjoint (B : ∀ i, G i →ₗ[𝕜] G i) (hB : ∀ i, (B i).IsSymmetric) :
+    diracDirac B ≤ (diracDirac B)† :=
+  (diracDirac_isFormalAdjoint B hB).le_adjoint (dense_diracDomain B)
+
+/-- **The block-diagonal operator with symmetric blocks is self-adjoint.** The proof mirrors the
+circle/torus self-adjointness arguments: symmetry gives `D ≤ D†`, and testing the adjoint
+relation against each single-mode vector shows `D†.domain ⊆ diracDomain B`. -/
+theorem diracDirac_isSelfAdjoint (B : ∀ i, G i →ₗ[𝕜] G i) (hB : ∀ i, (B i).IsSymmetric) :
+    IsSelfAdjoint (diracDirac B) := by
+  classical
+  rw [LinearPMap.isSelfAdjoint_def]
+  have hfa : (diracDirac B)†.IsFormalAdjoint (diracDirac B) :=
+    LinearPMap.adjoint_isFormalAdjoint (dense_diracDomain B)
+  have hdomle : (diracDirac B)†.domain ≤ diracDomain B := by
+    intro y hy
+    rw [mem_diracDomain_iff]
+    have hcoe : (fun i => B i (y i)) = ⇑((diracDirac B)† ⟨y, hy⟩) := by
+      funext i
+      refine (ext_inner_right 𝕜 fun v => ?_).symm
+      have key := hfa ⟨y, hy⟩ ⟨lp.single 2 i v, single_mem_diracDomain B i v⟩
+      rw [lp.inner_single_right, diracDirac_single, lp.inner_single_right] at key
+      rw [key]
+      exact (hB i (y i) v).symm
+    rw [hcoe]; exact lp.memℓp _
+  have heq : (diracDirac B).domain = (diracDirac B)†.domain :=
+    le_antisymm (diracDirac_le_adjoint B hB).1 hdomle
+  exact (LinearPMap.eq_of_le_of_domain_eq (diracDirac_le_adjoint B hB) heq).symm
+
 end lpDiag
diff --git a/SpectralTriples/Examples/Circle.lean b/SpectralTriples/Examples/Circle.lean
index 0fc633b..f0791f9 100644
--- a/SpectralTriples/Examples/Circle.lean
+++ b/SpectralTriples/Examples/Circle.lean
@@ -76,123 +76,41 @@ eigenvalue is the real number `n`. These are real (hence `D` is symmetric) and s
 `|n| → ∞` (hence `D` has compact resolvent). -/
 def diracEigen : ℤ → ℝ := fun n => (n : ℝ)
 
+/-- The scalar block at Fourier mode `n`: multiplication by the real eigenvalue `n`, as an
+instance of the generic symmetric-block-diagonal machinery of `lpDiag`. -/
+noncomputable def diracBlock (n : ℤ) : ℂ →ₗ[ℂ] ℂ := (diracEigen n : ℂ) • LinearMap.id
+
+@[simp] theorem diracBlock_apply (n : ℤ) (v : ℂ) :
+    diracBlock n v = (diracEigen n : ℂ) * v :=
+  smul_eq_mul _ _
+
+/-- Each scalar block is symmetric, since its eigenvalue is real. -/
+theorem diracBlock_isSymmetric (n : ℤ) : (diracBlock n).IsSymmetric := by
+  intro x y
+  simp only [diracBlock_apply, RCLike.inner_apply, map_mul, Complex.conj_ofReal]
+  ring
+
 /-- The maximal domain of the circle Dirac operator: the `H¹` Sobolev space
 `{ a ∈ ℓ²(ℤ) : Σ n² |aₙ|² < ∞ }`, i.e. those `a` for which `n ↦ n · aₙ` is again in `ℓ²(ℤ)`.
 This is the domain on which the diagonal Dirac operator `(D a)ₙ = n · aₙ` will be defined. -/
-def diracDomain : Submodule ℂ L2 where
-  carrier := {a | Memℓp (fun n => (diracEigen n : ℂ) * a n) 2}
-  zero_mem' := by
-    simp only [Set.mem_setOf_eq, lp.coeFn_zero, Pi.zero_apply, mul_zero]
-    exact zero_memℓp
-  add_mem' := by
-    intro a b ha hb
-    simp only [Set.mem_setOf_eq, lp.coeFn_add, Pi.add_apply, mul_add] at *
-    exact ha.add hb
-  smul_mem' := by
-    intro c a ha
-    simp only [Set.mem_setOf_eq, lp.coeFn_smul, Pi.smul_apply, smul_eq_mul] at *
-    have hrw : (fun n => (diracEigen n : ℂ) * (c * a n))
-        = c • fun n => (diracEigen n : ℂ) * a n := by
-      funext n; simp only [Pi.smul_apply, smul_eq_mul]; ring
-    rw [hrw]; exact ha.const_smul c
+noncomputable def diracDomain : Submodule ℂ L2 := lpDiag.diracDomain diracBlock
 
 theorem mem_diracDomain_iff (a : L2) :
-    a ∈ diracDomain ↔ Memℓp (fun n => (diracEigen n : ℂ) * a n) 2 := Iff.rfl
-
-/-- Coordinatewise multiplication by the eigenvalue sequence `(n)`, as an element of `ℓ²(ℤ)`,
-given a proof that the result is square-summable. -/
-def applyDirac (a : L2) (h : Memℓp (fun n => (diracEigen n : ℂ) * a n) 2) : L2 :=
-  ⟨fun n => (diracEigen n : ℂ) * a n, h⟩
-
-@[simp] theorem coe_applyDirac (a : L2) (h) (n : ℤ) :
-    (applyDirac a h) n = (diracEigen n : ℂ) * a n := rfl
+    a ∈ diracDomain ↔ Memℓp (fun n => (diracEigen n : ℂ) * a n) 2 := by
+  simp only [diracDomain, lpDiag.mem_diracDomain_iff, diracBlock_apply]
 
 /-- The circle Dirac operator `D = -i d/dθ` as an unbounded `LinearPMap`: diagonal on the
 Fourier basis, `(D a)ₙ = n · aₙ`, with domain the `H¹` Sobolev space `diracDomain`. -/
-noncomputable def diracDirac : L2 →ₗ.[ℂ] L2 where
-  domain := diracDomain
-  toFun :=
-    { toFun := fun a => applyDirac (a : L2) ((mem_diracDomain_iff _).mp a.2)
-      map_add' := fun a b => by
-        ext n
-        simp only [coe_applyDirac, Submodule.coe_add, lp.coeFn_add, Pi.add_apply, mul_add]
-      map_smul' := fun c a => by
-        ext n
-        simp only [coe_applyDirac, Submodule.coe_smul, lp.coeFn_smul, Pi.smul_apply,
-          smul_eq_mul, RingHom.id_apply, mul_left_comm] }
+noncomputable def diracDirac : L2 →ₗ.[ℂ] L2 := lpDiag.diracDirac diracBlock
 
 @[simp] theorem diracDirac_apply (a : diracDomain) (n : ℤ) :
-    (diracDirac a) n = (diracEigen n : ℂ) * (a : L2) n := rfl
+    (diracDirac a) n = (diracEigen n : ℂ) * (a : L2) n := by
+  simp only [diracDirac, lpDiag.diracDirac_apply, diracBlock_apply]
 
-/-- The circle Dirac operator is symmetric (formally self-adjoint): `⟪D x, y⟫ = ⟪x, D y⟫`
-on its domain, because its eigenvalues are real. -/
-theorem diracDirac_isFormalAdjoint : diracDirac.IsFormalAdjoint diracDirac := by
-  intro x y
-  rw [lp.inner_eq_tsum, lp.inner_eq_tsum]
-  refine tsum_congr fun n => ?_
-  simp only [diracDirac_apply, RCLike.inner_apply, map_mul, Complex.conj_ofReal]
-  ring
-
-/-- Each Fourier basis vector `eₙ = lp.single 2 n 1` lies in the `H¹` domain (it has finite
-support, so `m ↦ m · (eₙ)ₘ = n · eₙ` is square-summable). -/
-theorem single_mem_diracDomain (n : ℤ) : (lp.single 2 n (1 : ℂ) : L2) ∈ diracDomain := by
-  rw [mem_diracDomain_iff]
-  have hfun : (fun m => (diracEigen m : ℂ) * (lp.single 2 n (1 : ℂ) : L2) m)
-      = (diracEigen n : ℂ) • (⇑(lp.single 2 n (1 : ℂ) : L2) : ℤ → ℂ) := by
-    funext m
-    rcases eq_or_ne m n with h | h
-    · subst h; simp [lp.single_apply]
-    · simp [lp.single_apply, h]
-  rw [hfun]
-  exact (lp.memℓp _).const_smul _
-
-/-- The `H¹` domain is dense in `ℓ²(ℤ)`: it contains every Fourier basis vector, so its
-orthogonal complement is trivial. -/
-theorem dense_diracDomain : Dense (diracDirac.domain : Set L2) := by
-  change Dense (diracDomain : Set L2)
-  have horth : (diracDomain : Submodule ℂ L2)ᗮ = ⊥ := by
-    rw [Submodule.eq_bot_iff]
-    intro y hy
-    refine lp.ext (funext fun n => ?_)
-    have h0 : inner ℂ (lp.single 2 n (1 : ℂ) : L2) y = 0 := hy _ (single_mem_diracDomain n)
-    rw [lp.inner_single_left] at h0
-    simpa [RCLike.inner_apply, lp.coeFn_zero] using h0
-  have htop : diracDomain.topologicalClosure = ⊤ :=
-    (Submodule.topologicalClosure_eq_top_iff (K := diracDomain)).mpr horth
-  rw [dense_iff_closure_eq, ← Submodule.topologicalClosure_coe, htop, Submodule.top_coe]
-
-/-- The circle Dirac operator is contained in its adjoint (symmetry ⇒ `D ≤ D†`). -/
-theorem diracDirac_le_adjoint : diracDirac ≤ diracDirac† :=
-  diracDirac_isFormalAdjoint.le_adjoint dense_diracDomain
-
-/-- **The circle Dirac operator is self-adjoint.** Since it is symmetric (so `D ≤ D†`), it
-suffices that `D†.domain ⊆ D.domain`: for `y ∈ D†.domain`, testing the adjoint relation against
-each Fourier basis vector `eₙ` gives `(D† y)ₙ = n · yₙ`, so `n ↦ n · yₙ` is square-summable and
-`y` lies in the `H¹` domain. -/
-theorem diracDirac_isSelfAdjoint : IsSelfAdjoint diracDirac := by
-  rw [isSelfAdjoint_def]
-  have hfa : diracDirac†.IsFormalAdjoint diracDirac := adjoint_isFormalAdjoint dense_diracDomain
-  have hdomle : diracDirac†.domain ≤ diracDomain := by
-    intro y hy
-    rw [mem_diracDomain_iff]
-    have hcoe : (fun n => (diracEigen n : ℂ) * y n) = ⇑(diracDirac† ⟨y, hy⟩) := by
-      funext n
-      have key := hfa ⟨y, hy⟩ ⟨lp.single 2 n (1 : ℂ), single_mem_diracDomain n⟩
-      have hDe : diracDirac ⟨lp.single 2 n (1 : ℂ), single_mem_diracDomain n⟩
-          = (diracEigen n : ℂ) • (lp.single 2 n (1 : ℂ) : L2) := by
-        refine lp.ext (funext fun m => ?_)
-        simp only [diracDirac_apply, lp.coeFn_smul, Pi.smul_apply, smul_eq_mul]
-        rcases eq_or_ne m n with h | h
-        · subst h; rfl
-        · simp [lp.single_apply, h]
-      rw [lp.inner_single_right, hDe, inner_smul_right, lp.inner_single_right] at key
-      have key2 := congrArg (starRingEnd ℂ) key
-      simp [RCLike.inner_apply, map_mul, Complex.conj_ofReal] at key2
-      exact key2.symm
-    rw [hcoe]; exact lp.memℓp _
-  have heq : diracDirac.domain = diracDirac†.domain :=
-    le_antisymm diracDirac_le_adjoint.1 hdomle
-  exact (LinearPMap.eq_of_le_of_domain_eq diracDirac_le_adjoint heq).symm
+/-- **The circle Dirac operator is self-adjoint.** An instance of the generic
+`lpDiag.diracDirac_isSelfAdjoint` for symmetric block families. -/
+theorem diracDirac_isSelfAdjoint : IsSelfAdjoint diracDirac :=
+  lpDiag.diracDirac_isSelfAdjoint diracBlock diracBlock_isSymmetric
 
 /-- `i` lies in the resolvent set of the circle Dirac operator: it is self-adjoint and
 `Im i = 1 ≠ 0`, so the basic criterion applies. -/
diff --git a/SpectralTriples/Examples/Shift.lean b/SpectralTriples/Examples/Shift.lean
index 07e8aa1..e0440a5 100644
--- a/SpectralTriples/Examples/Shift.lean
+++ b/SpectralTriples/Examples/Shift.lean
@@ -9,6 +9,7 @@ module
 public import Mathlib.Analysis.InnerProductSpace.l2Space
 public import Mathlib.LinearAlgebra.FiniteDimensional.Basic
 public import SpectralTriples.Fredholm
+public import SpectralTriples.CompactOperators
 
 /-! # The unilateral shift on `ℓ²(ℕ)`
 
@@ -190,19 +191,6 @@ theorem range_shift_orthogonal_finrank :
   rw [range_shift_orthogonal]
   exact finrank_span_singleton e0_ne_zero
 
-/-- For a closed range in a Hilbert space, the quotient cokernel has the same dimension as the
-orthogonal-complement cokernel. -/
-theorem finrank_quotient_range_eq_orthogonal {H : Type*} [NormedAddCommGroup H]
-    [InnerProductSpace ℂ H] [CompleteSpace H] (T : H →L[ℂ] H)
-    (hclosed : IsClosed (LinearMap.range (T : H →ₗ[ℂ] H) : Set H)) :
-    Module.finrank ℂ (H ⧸ LinearMap.range (T : H →ₗ[ℂ] H))
-      = Module.finrank ℂ (LinearMap.range (T : H →ₗ[ℂ] H))ᗮ := by
-  let K : Submodule ℂ H := LinearMap.range (T : H →ₗ[ℂ] H)
-  change Module.finrank ℂ (H ⧸ K) = Module.finrank ℂ ↥Kᗮ
-  haveI : CompleteSpace K := hclosed.completeSpace_coe
-  exact (Submodule.quotientEquivOfIsCompl K Kᗮ
-    Submodule.isCompl_orthogonal_of_hasOrthogonalProjection).finrank_eq
-
 /-- The range of the unilateral shift is closed. -/
 theorem isClosed_range_shift :
     IsClosed (LinearMap.range (shift : H →ₗ[ℂ] H) : Set H) := by
@@ -222,9 +210,11 @@ theorem isClosed_range_shift :
 /-- The forward unilateral shift on `ℓ²(ℕ)` is Fredholm of index `-1`. -/
 theorem fredholmIndex_shift :
     SpectralTriples.Fredholm.index (shift : H →ₗ[ℂ] H) = -1 := by
+  haveI : CompleteSpace (LinearMap.range (shift : H →ₗ[ℂ] H)) :=
+    isClosed_range_shift.completeSpace_coe
   unfold SpectralTriples.Fredholm.index
   rw [shift_ker_eq_bot, finrank_bot,
-    finrank_quotient_range_eq_orthogonal shift isClosed_range_shift,
+    (LinearMap.range (shift : H →ₗ[ℂ] H)).finrank_quotient_eq_finrank_orthogonal,
     range_shift_orthogonal_finrank]
   norm_num
 
diff --git a/SpectralTriples/Examples/Torus.lean b/SpectralTriples/Examples/Torus.lean
index d0c523d..f917016 100644
--- a/SpectralTriples/Examples/Torus.lean
+++ b/SpectralTriples/Examples/Torus.lean
@@ -98,52 +98,6 @@ noncomputable def diracBlock (p : ℤ × ℤ) : Spinor →ₗ[ℂ] Spinor :=
     !![0, (p.1 : ℂ) - (p.2 : ℂ) * Complex.I;
        (p.1 : ℂ) + (p.2 : ℂ) * Complex.I, 0]
 
-/-- The maximal domain of the torus Dirac operator: the `H¹` Sobolev space, those `a` for which
-`p ↦ D₍ₚ₎ (aₚ)` is again square-summable (equivalently `Σ (m²+n²) ‖aₚ‖² < ∞`). -/
-def diracDomain : Submodule ℂ H where
-  carrier := {a | Memℓp (fun p => diracBlock p (a p)) 2}
-  zero_mem' := by
-    have : (fun p => diracBlock p ((0 : H) p)) = 0 := by
-      funext p; simp only [lp.coeFn_zero, Pi.zero_apply, _root_.map_zero]
-    simp only [Set.mem_setOf_eq, this]; exact zero_memℓp
-  add_mem' := fun {a b} ha hb => by
-    have heq : (fun p => diracBlock p ((a + b) p))
-        = (fun p => diracBlock p (a p)) + fun p => diracBlock p (b p) := by
-      funext p; simp only [lp.coeFn_add, Pi.add_apply, _root_.map_add]
-    rw [Set.mem_setOf_eq, heq]; exact ha.add hb
-  smul_mem' := fun c a ha => by
-    have heq : (fun p => diracBlock p ((c • a) p)) = c • fun p => diracBlock p (a p) := by
-      funext p; simp only [lp.coeFn_smul, Pi.smul_apply, _root_.map_smul]
-    rw [Set.mem_setOf_eq, heq]; exact ha.const_smul c
-
-theorem mem_diracDomain_iff (a : H) :
-    a ∈ diracDomain ↔ Memℓp (fun p => diracBlock p (a p)) 2 := Iff.rfl
-
-/-- Coordinatewise application of the Dirac blocks, as an element of `ℓ²(ℤ²; ℂ²)`, given a
-proof that the result is square-summable. -/
-noncomputable def applyDirac (a : H) (h : Memℓp (fun p => diracBlock p (a p)) 2) : H :=
-  ⟨fun p => diracBlock p (a p), h⟩
-
-@[simp] theorem coe_applyDirac (a : H) (h) (p : ℤ × ℤ) :
-    (applyDirac a h) p = diracBlock p (a p) := rfl
-
-/-- The torus Dirac operator as an unbounded `LinearPMap`: block-diagonal on the Fourier
-lattice, `(D a)₍ₘ,ₙ₎ = D₍ₘ,ₙ₎ (a₍ₘ,ₙ₎)`, with domain the `H¹` Sobolev space `diracDomain`. -/
-noncomputable def diracDirac : H →ₗ.[ℂ] H where
-  domain := diracDomain
-  toFun :=
-    { toFun := fun a => applyDirac (a : H) ((mem_diracDomain_iff _).mp a.2)
-      map_add' := fun a b => by
-        refine lp.ext (funext fun p => ?_)
-        simp only [coe_applyDirac, Submodule.coe_add, lp.coeFn_add, Pi.add_apply, _root_.map_add]
-      map_smul' := fun c a => by
-        refine lp.ext (funext fun p => ?_)
-        simp only [coe_applyDirac, Submodule.coe_smul, lp.coeFn_smul, Pi.smul_apply,
-          _root_.map_smul, RingHom.id_apply] }
-
-@[simp] theorem diracDirac_apply (a : diracDomain) (p : ℤ × ℤ) :
-    (diracDirac a) p = diracBlock p ((a : H) p) := rfl
-
 /-- Each Dirac block is self-adjoint on the spinor fibre: the matrix
 `2π·!![0, m-in; m+in, 0]` is Hermitian. -/
 theorem diracBlock_isSymmetric (p : ℤ × ℤ) : (diracBlock p).IsSymmetric := by
@@ -152,80 +106,27 @@ theorem diracBlock_isSymmetric (p : ℤ × ℤ) : (diracBlock p).IsSymmetric :=
   fin_cases i <;> fin_cases j <;>
     simp [Matrix.conjTranspose_apply, Matrix.smul_apply, Complex.conj_ofReal, sub_eq_add_neg]
 
-/-- The torus Dirac operator is symmetric (formally self-adjoint): `⟪D a, b⟫ = ⟪a, D b⟫` on its
-domain, because each spinor block is self-adjoint. -/
-theorem diracDirac_isFormalAdjoint : diracDirac.IsFormalAdjoint diracDirac := by
-  intro a b
-  rw [lp.inner_eq_tsum, lp.inner_eq_tsum]
-  refine tsum_congr fun p => ?_
-  rw [diracDirac_apply, diracDirac_apply]
-  exact diracBlock_isSymmetric p _ _
-
-/-- Each `lp.single (m, n) v` (a single spinor in one Fourier mode) lies in the `H¹` domain: it
-has finite support, so `q ↦ D₍q₎ (single₍q₎)` is supported on `{(m, n)}` and square-summable. -/
-theorem single_mem_diracDomain (p : ℤ × ℤ) (v : Spinor) :
-    (lp.single 2 p v : H) ∈ diracDomain := by
-  rw [mem_diracDomain_iff]
-  have hfun : (fun q => diracBlock q ((lp.single 2 p v : H) q))
-      = ⇑(lp.single 2 p (diracBlock p v) : H) := by
-    funext q
-    rcases eq_or_ne q p with h | h
-    · subst h; simp [lp.single_apply]
-    · simp [lp.single_apply, h, _root_.map_zero]
-  rw [hfun]
-  exact lp.memℓp _
+/-- The maximal domain of the torus Dirac operator: the `H¹` Sobolev space, those `a` for which
+`p ↦ D₍ₚ₎ (aₚ)` is again square-summable (equivalently `Σ (m²+n²) ‖aₚ‖² < ∞`). An instance of
+the generic symmetric-block-diagonal machinery of `lpDiag`. -/
+noncomputable def diracDomain : Submodule ℂ H := lpDiag.diracDomain diracBlock
 
-/-- The image `D (single (m, n) v) = single (m, n) (D₍ₘ,ₙ₎ v)`: the block-diagonal operator acts
-on a single-mode vector by its block in that mode. -/
-theorem diracDirac_single (p : ℤ × ℤ) (v : Spinor) :
-    diracDirac ⟨lp.single 2 p v, single_mem_diracDomain p v⟩
-      = (lp.single 2 p (diracBlock p v) : H) := by
-  refine lp.ext (funext fun q => ?_)
-  rcases eq_or_ne q p with h | h
-  · subst h; simp [diracDirac_apply, lp.single_apply]
-  · simp [diracDirac_apply, lp.single_apply, h, _root_.map_zero]
-
-/-- The `H¹` domain is dense in `ℓ²(ℤ²; ℂ²)`: it contains every single-mode spinor, so its
-orthogonal complement is trivial. -/
-theorem dense_diracDomain : Dense (diracDirac.domain : Set H) := by
-  change Dense (diracDomain : Set H)
-  have horth : (diracDomain : Submodule ℂ H)ᗮ = ⊥ := by
-    rw [Submodule.eq_bot_iff]
-    intro y hy
-    refine lp.ext (funext fun p => ?_)
-    refine ext_inner_left ℂ fun v => ?_
-    have h0 : inner ℂ (lp.single 2 p v : H) y = 0 := hy _ (single_mem_diracDomain p v)
-    rw [lp.inner_single_left] at h0
-    rw [h0, lp.coeFn_zero, Pi.zero_apply, inner_zero_right]
-  have htop : diracDomain.topologicalClosure = ⊤ :=
-    (Submodule.topologicalClosure_eq_top_iff (K := diracDomain)).mpr horth
-  rw [dense_iff_closure_eq, ← Submodule.topologicalClosure_coe, htop, Submodule.top_coe]
-
-/-- The torus Dirac operator is contained in its adjoint (symmetry ⇒ `D ≤ D†`). -/
-theorem diracDirac_le_adjoint : diracDirac ≤ diracDirac† :=
-  diracDirac_isFormalAdjoint.le_adjoint dense_diracDomain
-
-/-- **The torus Dirac operator is self-adjoint.** It is symmetric (so `D ≤ D†`); it remains to
-show `D†.domain ⊆ D.domain`. For `y ∈ D†.domain`, testing the adjoint relation against each
-single-mode spinor `single (m, n) v` and using self-adjointness of the block gives
-`(D† y)₍ₘ,ₙ₎ = D₍ₘ,ₙ₎ (y₍ₘ,ₙ₎)`, so `q ↦ D₍q₎ (y₍q₎)` is square-summable and `y ∈ H¹`. -/
-theorem diracDirac_isSelfAdjoint : IsSelfAdjoint diracDirac := by
-  rw [isSelfAdjoint_def]
-  have hfa : diracDirac†.IsFormalAdjoint diracDirac := adjoint_isFormalAdjoint dense_diracDomain
-  have hdomle : diracDirac†.domain ≤ diracDomain := by
-    intro y hy
-    rw [mem_diracDomain_iff]
-    have hcoe : (fun p => diracBlock p (y p)) = ⇑(diracDirac† ⟨y, hy⟩) := by
-      funext p
-      refine (ext_inner_right ℂ fun v => ?_).symm
-      have key := hfa ⟨y, hy⟩ ⟨lp.single 2 p v, single_mem_diracDomain p v⟩
-      rw [lp.inner_single_right, diracDirac_single, lp.inner_single_right] at key
-      rw [key]
-      exact (diracBlock_isSymmetric p (y p) v).symm
-    rw [hcoe]; exact lp.memℓp _
-  have heq : diracDirac.domain = diracDirac†.domain :=
-    le_antisymm diracDirac_le_adjoint.1 hdomle
-  exact (LinearPMap.eq_of_le_of_domain_eq diracDirac_le_adjoint heq).symm
+theorem mem_diracDomain_iff (a : H) :
+    a ∈ diracDomain ↔ Memℓp (fun p => diracBlock p (a p)) 2 :=
+  lpDiag.mem_diracDomain_iff diracBlock a
+
+/-- The torus Dirac operator as an unbounded `LinearPMap`: block-diagonal on the Fourier
+lattice, `(D a)₍ₘ,ₙ₎ = D₍ₘ,ₙ₎ (a₍ₘ,ₙ₎)`, with domain the `H¹` Sobolev space `diracDomain`. -/
+noncomputable def diracDirac : H →ₗ.[ℂ] H := lpDiag.diracDirac diracBlock
+
+@[simp] theorem diracDirac_apply (a : diracDomain) (p : ℤ × ℤ) :
+    (diracDirac a) p = diracBlock p ((a : H) p) :=
+  lpDiag.diracDirac_apply diracBlock a p
+
+/-- **The torus Dirac operator is self-adjoint.** An instance of the generic
+`lpDiag.diracDirac_isSelfAdjoint` for symmetric block families. -/
+theorem diracDirac_isSelfAdjoint : IsSelfAdjoint diracDirac :=
+  lpDiag.diracDirac_isSelfAdjoint diracBlock diracBlock_isSymmetric
 
 /-- `i` lies in the resolvent set of the torus Dirac operator: it is self-adjoint and
 `Im i = 1 ≠ 0`, so the basic criterion applies. -/
diff --git a/audit/FAITHFULNESS.md b/audit/FAITHFULNESS.md
index 7fb7248..7186f72 100644
--- a/audit/FAITHFULNESS.md
+++ b/audit/FAITHFULNESS.md
@@ -64,9 +64,10 @@ representation `π : A →⋆ₐ[𝕜] (H →L[𝕜] H)`.
 
 | Object / Claim | Informal content | Lean | Status |
 |---|---|---|---|
-| Block-diagonal operator on `ℓ²` | `(diagL T) a = (i ↦ Tᵢ aᵢ)` for a uniformly bounded block family | `lpDiag.diagL` — `DiagonalOperator.lean:69` | ✓ axiom-clean |
-| its operator-norm bound | `‖diagL T‖ ≤ C` when `‖Tᵢ‖ ≤ C` | `lpDiag.norm_diagL_le` — `DiagonalOperator.lean:97` | ✓ axiom-clean |
-| **compactness criterion** | block norms `→ 0` (cofinite) + finite-dim fibres ⇒ `diagL T` compact (finite-rank truncations converge in operator norm) | `lpDiag.isCompactOperator_diagL` — `DiagonalOperator.lean:185` | ✓ axiom-clean |
+| Block-diagonal operator on `ℓ²` | `(diagL T) a = (i ↦ Tᵢ aᵢ)` for a uniformly bounded block family | `lpDiag.diagL` — `DiagonalOperator.lean:70` | ✓ axiom-clean |
+| its operator-norm bound | `‖diagL T‖ ≤ C` when `‖Tᵢ‖ ≤ C` | `lpDiag.norm_diagL_le` — `DiagonalOperator.lean:98` | ✓ axiom-clean |
+| **compactness criterion** | block norms `→ 0` (cofinite) + finite-dim fibres ⇒ `diagL T` compact (finite-rank truncations converge in operator norm) | `lpDiag.isCompactOperator_diagL` — `DiagonalOperator.lean:186` | ✓ axiom-clean |
+| **unbounded block-diagonal Dirac operator** | given symmetric blocks `B i`, the operator on its maximal `ℓ²` domain is self-adjoint (shared by the `S¹`/`T²` examples below) | `lpDiag.diracDirac_isSelfAdjoint` — `DiagonalOperator.lean:340` | ✓ axiom-clean |
 
 ## Index of an even spectral triple (Phase 2 foundations)
 
@@ -97,20 +98,20 @@ Reference: Connes Ch. VI; GBF §9–12 (canonical triple of a spin manifold, her
 
 | Object / Claim | Lean | Status |
 |---|---|---|
-| Dirac operator `D` (block-diagonal, unbounded) | `SpectralTriples.Torus.diracDirac` — `Examples/Torus.lean:131` | ✓ axiom-clean |
-| `D` self-adjoint | `SpectralTriples.Torus.diracDirac_isSelfAdjoint` — `Examples/Torus.lean:211` | ✓ axiom-clean |
-| `i ∈ ρ(D)` | `SpectralTriples.Torus.mem_resolventSet_I` — `Examples/Torus.lean:231` | ✓ axiom-clean |
-| `(D − i·1)⁻¹` is compact | `SpectralTriples.Torus.isCompactOperator_resolvent_I` — `Examples/Torus.lean:509` | ✓ axiom-clean |
-| grading `γ = σ₃` (CLM) | `SpectralTriples.Torus.grading` — `Examples/Torus.lean:592` | ✓ axiom-clean |
-| `γ` self-adjoint | `SpectralTriples.Torus.isSelfAdjoint_grading` — `Examples/Torus.lean:608` | ✓ axiom-clean |
-| `γ² = 1` | `SpectralTriples.Torus.grading_mul_self` — `Examples/Torus.lean:612` | ✓ axiom-clean |
-| `D γ = −γ D` on `dom D` | `SpectralTriples.Torus.grading_anticomm` — `Examples/Torus.lean:631` | ✓ axiom-clean |
-| algebra `ℂ[ℤ²]` (shift `*`-subalgebra) | `SpectralTriples.Torus.algebra` — `Examples/Torus.lean:871` | ✓ axiom-clean |
-| representation (inclusion `StarAlgHom`) | `SpectralTriples.Torus.rep` — `Examples/Torus.lean:876` | ✓ axiom-clean |
-| **`(A, H, D)` is an odd spectral triple** | `SpectralTriples.Torus.isOddSpectralTriple` — `Examples/Torus.lean:931` | ✓ axiom-clean |
-| **`(A, H, D, γ)` is an even spectral triple** | `SpectralTriples.Torus.isEvenSpectralTriple` — `Examples/Torus.lean:984` | ✓ axiom-clean |
-| **finitely summable at `i`** | `SpectralTriples.Torus.isFinitelySummableSpectralTriple` — `Examples/Torus.lean:994` | ✓ axiom-clean |
-| **index `= 0`** (`Â(T²)·rk`; `ker D = ℂ²` at the zero mode, split `1+1` by `γ`) | `SpectralTriples.Torus.index_eq_zero` — `Examples/Torus.lean:1257` | ✓ axiom-clean |
+| Dirac operator `D` (block-diagonal, unbounded) | `SpectralTriples.Torus.diracDirac` — `Examples/Torus.lean:120` | ✓ axiom-clean |
+| `D` self-adjoint | `SpectralTriples.Torus.diracDirac_isSelfAdjoint` — `Examples/Torus.lean:128` | ✓ axiom-clean |
+| `i ∈ ρ(D)` | `SpectralTriples.Torus.mem_resolventSet_I` — `Examples/Torus.lean:133` | ✓ axiom-clean |
+| `(D − i·1)⁻¹` is compact | `SpectralTriples.Torus.isCompactOperator_resolvent_I` — `Examples/Torus.lean:411` | ✓ axiom-clean |
+| grading `γ = σ₃` (CLM) | `SpectralTriples.Torus.grading` — `Examples/Torus.lean:494` | ✓ axiom-clean |
+| `γ` self-adjoint | `SpectralTriples.Torus.isSelfAdjoint_grading` — `Examples/Torus.lean:510` | ✓ axiom-clean |
+| `γ² = 1` | `SpectralTriples.Torus.grading_mul_self` — `Examples/Torus.lean:514` | ✓ axiom-clean |
+| `D γ = −γ D` on `dom D` | `SpectralTriples.Torus.grading_anticomm` — `Examples/Torus.lean:533` | ✓ axiom-clean |
+| algebra `ℂ[ℤ²]` (shift `*`-subalgebra) | `SpectralTriples.Torus.algebra` — `Examples/Torus.lean:773` | ✓ axiom-clean |
+| representation (inclusion `StarAlgHom`) | `SpectralTriples.Torus.rep` — `Examples/Torus.lean:778` | ✓ axiom-clean |
+| **`(A, H, D)` is an odd spectral triple** | `SpectralTriples.Torus.isOddSpectralTriple` — `Examples/Torus.lean:833` | ✓ axiom-clean |
+| **`(A, H, D, γ)` is an even spectral triple** | `SpectralTriples.Torus.isEvenSpectralTriple` — `Examples/Torus.lean:886` | ✓ axiom-clean |
+| **finitely summable at `i`** | `SpectralTriples.Torus.isFinitelySummableSpectralTriple` — `Examples/Torus.lean:896` | ✓ axiom-clean |
+| **index `= 0`** (`Â(T²)·rk`; `ker D = ℂ²` at the zero mode, split `1+1` by `γ`) | `SpectralTriples.Torus.index_eq_zero` — `Examples/Torus.lean:1158` | ✓ axiom-clean |
 
 *Faithfulness note for the example.* The chosen algebra is the trigonometric polynomials
 `ℂ[ℤ²]` (Fourier dual of `C(T²)`), represented by the coordinate shift unitaries — the
diff --git a/audit/axiom-report.txt b/audit/axiom-report.txt
index a2ab0ff..7668e09 100644
--- a/audit/axiom-report.txt
+++ b/audit/axiom-report.txt
@@ -25,6 +25,14 @@
 'SpectralTriples.Fredholm.index' depends on axioms: [propext, Classical.choice, Quot.sound]
 'SpectralTriples.Fredholm.isFredholm_of_bijective' depends on axioms: [propext, Classical.choice, Quot.sound]
 'SpectralTriples.Fredholm.index_of_bijective' depends on axioms: [propext, Classical.choice, Quot.sound]
+'IsCompactOperator.exists_finiteRank_norm_sub_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
+'ContinuousLinearMap.finiteDimensional_range_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
+'IsCompactOperator.adjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
+'Submodule.finrank_quotient_eq_finrank_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
+'Submodule.finiteDimensional_quotient_of_finiteDimensional_orthogonal' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound]
+'SpectralTriples.Fredholm.isFredholm_one_sub' depends on axioms: [propext, Classical.choice, Quot.sound]
 'SpectralTriples.Dkernel' depends on axioms: [propext, Classical.choice, Quot.sound]
 'SpectralTriples.index' depends on axioms: [propext, Classical.choice, Quot.sound]
 'SpectralTriples.finiteDimensional_Dkernel' depends on axioms: [propext, Classical.choice, Quot.sound]
@@ -62,7 +70,6 @@
 'SpectralTriples.Torus.isFinitelySummableSpectralTriple' depends on axioms: [propext, Classical.choice, Quot.sound]
 'SpectralTriples.Torus.index_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
 'SpectralTriples.Shift.shift' depends on axioms: [propext, Classical.choice, Quot.sound]
-'SpectralTriples.Shift.finrank_quotient_range_eq_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
 'SpectralTriples.Shift.fredholmIndex_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
 'SpectralTriples.MagneticDirac.magneticDirac' depends on axioms: [propext, Classical.choice, Quot.sound]
 'SpectralTriples.MagneticDirac.magneticDirac_ker_finrank' depends on axioms: [propext, Classical.choice, Quot.sound]
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
index 99f599b..1968694 100644
--- a/blueprint/src/content.tex
+++ b/blueprint/src/content.tex
@@ -217,10 +217,12 @@ \section{Fredholm operators}
 \subsection{Compact perturbations of the identity}
 \label{subsec:compact-perturbations}
 
-This subsection proves the Hilbert-space case of the classical Riesz--Schauder theorem:
-$1 - K$ is Fredholm whenever $K$ is compact. None of this is yet in Mathlib (only the weaker
-spectral dichotomy for compact operators is), so it is built here from scratch, as the
-analytic ingredient needed to eventually show the chiral Dirac operator $D^{+}$ is Fredholm.
+This subsection proves the structural part of the Hilbert-space case of the classical
+Riesz--Schauder theorem: $1 - K$ is Fredholm whenever $K$ is compact (finite kernel, closed
+range, finite-dimensional cokernel). The further classical fact that the index is $0$ is not
+proved here. None of this is yet in Mathlib (only the weaker spectral dichotomy for compact
+operators is), so it is built here from scratch, as the analytic ingredient needed to
+eventually show the chiral Dirac operator $D^{+}$ is Fredholm.
 
 \begin{theorem}[Compact operators are approximable by finite rank]
   \label{thm:exists-finiteRank-norm-sub-lt}
@@ -355,9 +357,11 @@ \chapter{Examples}
 triple; the two-torus example (Section~\ref{sec:torus}) is a complete, finitely summable, even
 spectral triple with vanishing index. Sections~\ref{sec:shift} and~\ref{sec:magnetic-dirac} give
 two further examples with \emph{nonzero} Fredholm index, $-1$ and $k$ respectively, completing
-the index arc $0, -1, k$. Section~\ref{sec:theta-sections} begins connecting the abstract
-flux-$k$ model of Section~\ref{sec:magnetic-dirac} back to genuine geometry, by exhibiting $k$
-independent holomorphic sections of the degree-$k$ line bundle on the square torus.
+the index arc $0, -1, k$. Sections~\ref{sec:theta-sections} and~\ref{sec:fourier-holomorphic}
+connect the abstract flux-$k$ model of Section~\ref{sec:magnetic-dirac} back to genuine
+geometry: together they give a complete, purely algebraic dimension count
+$\dim H^0(L_k) = k$, $\dim H^1(L_k) = 0$ for the degree-$k$ line bundle on the square torus,
+with no index theorem and no $L^2$ analysis.
 
 \section{Block-diagonal operators on \texorpdfstring{$\ell^2$}{l2}}
 \label{sec:diagonal-operators}
@@ -684,15 +688,17 @@ \section{The flux-\texorpdfstring{$k$}{k} magnetic Dirac model}
 \section{Theta sections on the square torus}
 \label{sec:theta-sections}
 
-\textbf{Status: partial (lower bound only).} This section proves the lower-bound half of the
+\textbf{Status: complete (lower bound).} This section proves the lower-bound half of the
 square-torus flux-$k$ Landau-level computation directly on the geometric side: $k$ explicit
 holomorphic theta sections for the degree-$k$ line bundle on the square torus $\mathbb{C} /
 (\mathbb{Z} + i \mathbb{Z})$ are exhibited and shown linearly independent, giving $\dim \ker
 D^{+} \geq k$ for the \emph{geometric} Dirac operator twisted by the degree-$k$ bundle (as
 opposed to the magnetic-translation model of Section~\ref{sec:magnetic-dirac}). The matching
-upper bound $\dim \ker D^{+} \leq k$, the vanishing of the cokernel, and the resulting
-identification of the geometric index with the model index $k$
-(Theorem~\ref{thm:fredholmIndex-magneticDirac}) are deferred; see
+upper bound $\dim \ker D^{+} \leq k$ and the vanishing of the cokernel are completed in
+Section~\ref{sec:fourier-holomorphic}. The resulting identification of the geometric index
+with the model index $k$ (Theorem~\ref{thm:fredholmIndex-magneticDirac}) — which additionally
+needs the $L^2$-to-holomorphic bridge (elliptic regularity for $\bar\partial$, not in Mathlib)
+and the unitary equivalence to the magnetic model — is deferred; see
 \texttt{SpectralTriples/docs/INDEX\_PAIRING.md} for the roadmap.
 
 \begin{definition}[Explicit degree-$k$ theta sections]
@@ -746,3 +752,122 @@ \section{Theta sections on the square torus}
   eigenvalues $\omega_k^{0}, \dots, \omega_k^{k-1}$ (the $k$ distinct $k$-th roots of unity),
   hence independent.
 \end{theorem}
+
+\section{The Fourier-coefficient recursion: an exact dimension count}
+\label{sec:fourier-holomorphic}
+
+\textbf{Status: complete (M3a, M3b).} This section completes the dimension count begun in
+Section~\ref{sec:theta-sections} (M2) by an entirely algebraic route, with \emph{no index
+theorem and no $L^2$ analysis}: the upper bound $\dim H^0(L_k) \leq k$ (M3a) and the
+cokernel vanishing $\dim H^1(L_k) = 0$ (M3b). Both rest on a single new analytic lemma not in
+Mathlib — the \emph{contour shift} — from which a Fourier-coefficient recursion is derived
+algebraically. See \texttt{SpectralTriples/docs/INDEX\_PAIRING.md} for the full roadmap; the
+remaining gap (M3c/M4: the $L^2$-to-holomorphic bridge and the unitary equivalence to the
+magnetic model of Section~\ref{sec:magnetic-dirac}) is the genuinely analytic frontier and is
+not addressed here.
+
+\begin{theorem}[Contour shift]
+  \label{thm:periodIntegral-eq-of-periodic}
+  \lean{SpectralTriples.periodIntegral_eq_of_periodic}
+  \leanok
+  For an entire $1$-periodic function $f$, the period integral $\int_0^1 f(x+iy)\,dx$ does not
+  depend on the height $y$. (Cauchy--Goursat on the rectangle $[0,1] \times [y_1,y_2]$: the two
+  vertical sides cancel by periodicity, leaving the two horizontal integrals equal.)
+\end{theorem}
+
+\begin{definition}[Holomorphic sections of the degree-$k$ line bundle]
+  \label{def:holSection}
+  \lean{SpectralTriples.holSection}
+  \leanok
+  $H^0(L_k)$: the space of entire functions $f$ with $f(z+1) = f(z)$ and the degree-$k$
+  automorphy factor $f(z+i) = e^{-\pi i k(2z+i)} f(z)$ — the same quasi-periodicity conditions
+  satisfied by the theta sections of Definition~\ref{def:thetaSection}.
+\end{definition}
+
+\begin{definition}[Fourier coefficient of a periodic holomorphic function]
+  \label{def:holCoeff}
+  \lean{SpectralTriples.holCoeff}
+  \leanok
+  For a $1$-periodic function $f$, the Fourier coefficient $a_m = \int_0^1 f(x)\,
+  e^{-2\pi i m x}\,dx$, computed on the real period.
+\end{definition}
+
+\begin{lemma}[The Fourier-coefficient recursion]
+  \label{lem:holCoeff-recursion}
+  \lean{SpectralTriples.holCoeff_recursion}
+  \leanok
+  \uses{def:holSection, def:holCoeff, thm:periodIntegral-eq-of-periodic}
+  For $f \in H^0(L_k)$, the Fourier coefficients satisfy
+  \[
+    a_{m+k} = e^{-\pi(2m+k)} \, a_m.
+  \]
+  Comparing Fourier coefficients of the degree-$k$ automorphy relation, via the contour shift
+  (Theorem~\ref{thm:periodIntegral-eq-of-periodic}) relating $f$'s Fourier coefficients on
+  different horizontal lines, turns the quasi-periodicity condition into this purely algebraic
+  recursion: the whole coefficient sequence is determined by $(a_0, \dots, a_{k-1})$.
+\end{lemma}
+
+\begin{theorem}[Fourier completeness: vanishing coefficients imply $f = 0$]
+  \label{thm:eq-zero-of-holCoeff-eq-zero}
+  \lean{SpectralTriples.eq_zero_of_holCoeff_eq_zero}
+  \leanok
+  \uses{def:holCoeff}
+  If $f$ is entire and $1$-periodic with all Fourier coefficients $a_m = 0$, then $f = 0$:
+  lifting $f$ to the circle, Mathlib's Fourier completeness gives $f$ vanishes on $\mathbb{R}$,
+  and the identity theorem for the entire function $f$ then gives $f \equiv 0$ on $\mathbb{C}$.
+\end{theorem}
+
+\begin{theorem}[The upper bound: $\dim H^0(L_k) \leq k$]
+  \label{thm:holSection-finrank-le}
+  \lean{SpectralTriples.holSection_finrank_le}
+  \leanok
+  \uses{lem:holCoeff-recursion, thm:eq-zero-of-holCoeff-eq-zero}
+  The restriction map $f \mapsto (a_0, \dots, a_{k-1})$ is an injective linear map
+  $H^0(L_k) \to \mathbb{C}^k$: by the recursion (Lemma~\ref{lem:holCoeff-recursion}),
+  $a_0 = \cdots = a_{k-1} = 0$ forces every Fourier coefficient to vanish, hence $f = 0$ by
+  Theorem~\ref{thm:eq-zero-of-holCoeff-eq-zero}. Injectivity gives $\dim H^0(L_k) \leq k$.
+\end{theorem}
+
+\begin{theorem}[The exact count: $\dim H^0(L_k) = k$]
+  \label{thm:holSection-finrank-eq}
+  \lean{SpectralTriples.holSection_finrank_eq}
+  \leanok
+  \uses{thm:holSection-finrank-le, thm:thetaSection-linearIndependent}
+  Combining the upper bound of Theorem~\ref{thm:holSection-finrank-le} (M3a) with the lower
+  bound of Theorem~\ref{thm:thetaSection-linearIndependent} (M2, the theta sections span a
+  $k$-dimensional subspace) gives $\dim H^0(L_k) = k$ exactly — a complete dimension theorem
+  with no index theorem and no $L^2$ analysis.
+\end{theorem}
+
+\begin{definition}[Holomorphic sections of the degree-$(-k)$ line bundle]
+  \label{def:holSectionNeg}
+  \lean{SpectralTriples.holSectionNeg}
+  \leanok
+  $H^0(L_{-k})$: the same definition as $H^0(L_k)$ (Definition~\ref{def:holSection}) but with
+  the opposite-sign automorphy factor $f(z+i) = e^{\pi i k(2z+i)} f(z)$. By Serre duality this
+  represents $H^1(L_k)$, the cokernel of the degree-$k$ Dirac operator.
+\end{definition}
+
+\begin{lemma}[Parseval decay of Fourier coefficients]
+  \label{lem:holCoeff-tendsto-atTop-zero}
+  \lean{SpectralTriples.holCoeff_tendsto_atTop_zero}
+  \leanok
+  \uses{def:holCoeff}
+  For any entire $1$-periodic $f$, the Fourier coefficients $a_m \to 0$ as $m \to \infty$ (and
+  as $m \to -\infty$): a consequence of $\ell^2$-summability of $|a_m|^2$ (Parseval, via the
+  $L^2$ lift to the circle).
+\end{lemma}
+
+\begin{theorem}[The cokernel vanishes: $\dim H^0(L_{-k}) = 0$]
+  \label{thm:holSectionNeg-eq-bot}
+  \lean{SpectralTriples.holSectionNeg_eq_bot, SpectralTriples.holSectionNeg_finrank_eq_zero}
+  \leanok
+  \uses{def:holSectionNeg, lem:holCoeff-recursion, lem:holCoeff-tendsto-atTop-zero,
+        thm:eq-zero-of-holCoeff-eq-zero}
+  $H^0(L_{-k}) = 0$ for $k > 0$ (equivalently $\dim H^1(L_k) = 0$, the cokernel-vanishing half
+  of $\operatorname{index} = k$, via Serre duality $h^1(L_k) = h^0(L_k^{-1})$). The
+  opposite-sign automorphy gives the opposite-sign recursion $a_{m+k} = e^{\pi(2m+k)} a_m$,
+  whose growth factor has modulus $> 1$; this clashes with the Parseval decay of
+  Lemma~\ref{lem:holCoeff-tendsto-atTop-zero} unless every coefficient is already $0$, and then
+  Theorem~\ref{thm:eq-zero-of-holCoeff-eq-zero} gives $f = 0$.
+\end{theorem}
diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex
index b9a1c18..e60d4ff 100644
--- a/blueprint/src/print.tex
+++ b/blueprint/src/print.tex
@@ -25,7 +25,7 @@
 \input{macros/print}
 
 \title{Spectral Triples and the Index Pairing}
-\author{Jon Bannon \and Michael R. Douglas}
+\author{Jon Bannon and Michael R. Douglas}
 
 \begin{document}
 \maketitle
diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex
index c64e36b..1344ddc 100644
--- a/blueprint/src/web.tex
+++ b/blueprint/src/web.tex
@@ -19,7 +19,7 @@
 \dochome{https://JonBannon.github.io/SpectralTriples/docs}
 
 \title{Spectral Triples and the Index Pairing}
-\author{Jon Bannon \and Michael R. Douglas}
+\author{Jon Bannon and Michael R. Douglas}
 
 \begin{document}
 \maketitle
diff --git a/scripts/axiom_report.lean b/scripts/axiom_report.lean
index 4e9a98a..80a6918 100644
--- a/scripts/axiom_report.lean
+++ b/scripts/axiom_report.lean
@@ -55,6 +55,15 @@ open LinearPMap
 #print axioms SpectralTriples.Fredholm.isFredholm_of_bijective
 #print axioms SpectralTriples.Fredholm.index_of_bijective
 
+-- CompactOperators.lean — compact operators on Hilbert space are Riesz–Schauder Fredholm
+-- perturbations of the identity (not yet in Mathlib).
+#print axioms IsCompactOperator.exists_finiteRank_norm_sub_lt
+#print axioms ContinuousLinearMap.finiteDimensional_range_adjoint
+#print axioms IsCompactOperator.adjoint
+#print axioms Submodule.finrank_quotient_eq_finrank_orthogonal
+#print axioms Submodule.finiteDimensional_quotient_of_finiteDimensional_orthogonal
+#print axioms SpectralTriples.Fredholm.isFredholm_one_sub
+
 -- Index.lean — the graded-kernel index of an even spectral triple.
 #print axioms SpectralTriples.Dkernel
 #print axioms SpectralTriples.index
@@ -105,7 +114,6 @@ open LinearPMap
 
 -- Examples/Shift.lean — the unilateral shift on ℓ²(ℕ): a Fredholm operator of index −1.
 #print axioms SpectralTriples.Shift.shift
-#print axioms SpectralTriples.Shift.finrank_quotient_range_eq_orthogonal
 #print axioms SpectralTriples.Shift.fredholmIndex_shift
 
 -- Examples/MagneticDirac.lean — flux-k magnetic Dirac model: index = k, with magnetic translations.