Lifting to a Box Domain (2D/3D)
Book 6's first three chapters all fixed d=1 deliberately. The question this chapter takes on is whether that was a genuine simplification or just a starting point — and the honest answer splits in two, one half settled here, one half still open pending an actual compile.
The discrete side: mechanical, verified this session
The heat equation chapter's discrete Laplacian Ah (Part II) is the standard 1D tridiagonal matrix. Its two-dimensional analogue on an N×N grid — the 5-point stencil finite-difference Laplacian on the box (0,1)² — is not a new object requiring new machinery. It is exactly the Kronecker sum of the same 1D matrix with itself:
and because Kronecker sums of symmetric matrices diagonalize in the tensor-product eigenbasis, the eigenvalues lift by simple addition: every 2D eigenvalue is a sum of two 1D eigenvalues from the heat equation chapter's own Prop. 12.1,
The conditioning bound is the genuinely interesting fact here: despite moving from 1 to 2 dimensions, κ(Ah(2D)) = Θ(h−2) — the same exponent as the 1D case, not h−4 or some dimension-dependent rate. Iterative solver cost still scales as O(h−1) CG iterations regardless of dimension, for this discretization. This is not obvious in advance; it falls directly out of the Kronecker structure once the eigenvalues are additive.
The continuous side: a real, still-open question
The harder half is whether the heat equation's Part I — the
H²₀(0,1) construction currently sitting behind an
axiom — lifts as cleanly. The reconnaissance into Scott Armstrong
and Julia Kempe's DeGiorgi Sobolev-space library found
real reason for optimism: their core definitions
(MemW1p, MemW1pWitness, MemW01p,
MemH01) are stated for Ω : Set E with
E := EuclideanSpace ℝ (Fin d) and d a fully
generic variable — no ball, no d ≥ 3 restriction
anywhere in that layer. A scratch test
(degiorgi-sobolev-scratch/DeGiorgiSobolevScratch/BoxDomainTest.lean)
applies their own memW01p_of_contDiff_hasCompactSupport_subset
lemma directly to a 2D box domain and to the exact 1D interval this
corpus already uses, producing two theorems
(boxBump2D_memH01, intervalBump1D_memH01)
that are not sorry — they are real applications of
the real, fetched lemma signature.
That test has not been compiled. It is a strong, source-grounded
reason to expect the lift works, not a proof that it does —
the scratch project needs an actual lake build, on a
separate Lean/Mathlib pin (v4.29.0-rc6) from this repo's own
(v4.14.0), which has not yet been run. Until it is, this chapter's
continuous half stays exactly where the reconnaissance left it:
plausible and specific, not confirmed.
| Statement | Status | Notes |
|---|---|---|
| 2D discrete Laplacian as Kronecker sum | verified numerically | Exact to machine precision against the 1D eigenvalue formula; not yet a Lean theorem |
| κ(Ah(2D)) = Θ(h−2) | verified numerically | Fitted slope −2.022 across six mesh sizes, matching the 1D result |
MemH01 domain-genericity (box, 2D and 1D) | written, not compiled | Real applications of DeGiorgi's own lemma; pending lake build |
| Full Parts I–III lift to 2D/3D | not started | Depends on the compile above; the discrete half (this chapter) is ready to receive it |