ch-atiyah showed the dm³ manifold retracts to S¹. The transverse linearisation along Γ is the scalar equation ρ′ = λρ with λ(z) = −2(1 − e−z), so the natural operator on the circle is
It is diagonal in the Fourier basis: einθ ↦ (in − a)einθ. A mode is killed exactly when in = a, and when a mode is killed it is also missing from the image. Kernel and cokernel have the same dimension at every a, so
Block [1] evaluates this at λ(0.5) = −0.786939, λ(8) = −1.999329, at the z → ∞ limit a = −2, at a = 0, and at the resonant a = 3i. Index 0 in every case, including the two where the kernel is non-trivial.
S¹ is a closed manifold of dimension 1, which is odd, and the index of any elliptic differential operator on a closed odd-dimensional manifold vanishes [standard]. So no differential operator anywhere on this circle will ever have a non-zero index. The search was closed before it started, and nothing about the dm³ dynamics enters the reason.
That standard statement covers differential operators. It does not cover pseudodifferential ones, and that gap is the entire escape route.
Take the Hardy space H² ⊂ L²(S¹) — the closed span of {einθ : n ≥ 0} — with the orthogonal projection P onto it. For a symbol f : S¹ → ℂ×, the Toeplitz operator is Tfu = P(f·u). For f = eikθ it acts on the basis by
This is a zeroth-order pseudodifferential operator, not a differential one, and it is Fredholm. Counting basis vectors — block [3], exactly, with no arithmetic to round:
| k | dim ker | dim coker | index |
|---|---|---|---|
| −3 | 3 | 0 | +3 |
| −1 | 1 | 0 | +1 |
| 0 | 0 | 0 | 0 |
| +1 | 0 | 1 | −1 |
| +3 | 0 | 3 | −3 |
Block [3] also re-runs it at truncations N = 50, 200 and 800 and gets the same integer, because the index is not a finite-section artefact — it is the one thing about an infinite-dimensional operator that a finite piece of it cannot show you.
What it is not is e−4π. The only non-zero indices this geometry admits are ∓ the winding number: integers, and for Γ that is −1. e−4π = 3.487342356×10−6 is not an integer, so it is not the index of anything, here or elsewhere.
WP-82's bar for Volume XI is “an index, computed, verified, and reported by the kernel.” ToeplitzIndex.lean does that, and needs no Mathlib to do it.
def toeplitz (k : Int) (n : Nat) : Option Nat :=
if 0 ≤ (n : Int) + k then some ((n : Int) + k).toNat else none
theorem mem_ker : toeplitz k n = none ↔ (n : Int) + k < 0
theorem mem_coker : (∀ n, toeplitz k n ≠ some m) ↔ (m : Int) < k
theorem toeplitz_index (k : Int) :
(kerCount k : Int) - (cokerCount k : Int) = -k
Two things about what that is and is not. It needs no Mathlib, which is a stronger position than the bar asked for — the dependency is Lean core and nothing else, so the file cannot drift with a Mathlib bump. And it formalises the count, not the analysis. The kernel now certifies that the kernel and cokernel of the basis action are the finite sets this chapter claims, and that their difference is −k for every k. That Tk is bounded, that it is Fredholm, that the index is a homotopy invariant, and Noether's theorem itself, are all still outside Lean — named in the file's own scope block before the first theorem.
So the arithmetic underneath Volume XI's index is kernel-reported, and the analytic content is not. That is a smaller claim than “Volume XI opens”, and it is the true one. [the count VERIFIED · the analysis OPEN]