discLap3
plain-language theorem explainer
The 3D discrete Laplacian on lattice tensor fields sums the three axis-aligned second-difference stencils, each scaled by N², acting componentwise on 3×3 complex matrices at sites of ℤ³. Flat-torus TT-spectrum and curved-operator underdetermination arguments cite it as the certified positive flat operator. The body is a direct finite-difference definition, not a derived identity.
Claim. For resolution $N\in\mathbb{N}$ and lattice tensor field $H:\mathbb{Z}^3\to M_3(\mathbb{C})$, the three-dimensional discrete Laplacian is $(\Delta_N H)(x)_{ij}=\sum_{a=0}^{2} N^2\bigl(H(x+e_a)_{ij}-2H(x)_{ij}+H(x-e_a)_{ij}\bigr)$, where $e_a$ are the three coordinate unit vectors.
background
This module closes Lane 4 of the Seven-Gaps campaign: operator convergence of the discrete TT perturbation spectrum to the continuum Lichnerowicz operator on the flat 3-torus. Lattice sites are Site3 = ℤ×ℤ×ℤ with N-periodicity along each axis (spacing h=1/N); tensor fields are maps to 3×3 complex matrices. Representation is deliberately on ℤ, not ZMod N, so stencil identities hold pointwise and periodicity is proved separately.
The spatial dimension is the forced D=3 of T8. Unit vectors unitVec a step one lattice unit along axis a. All convergence theorems in the file are restricted to the AXIS stencil sector: plane waves k=(k,0,0) acted on by this componentwise axis Laplacian. Panel mandate C14 flags that Freudenthal frozen energy is anisotropic, so axis stencils do not recover the full isotropic Lichnerowicz symbol.
Upstream, the 1D discrete Laplacian discLap and its Fourier eigenmode identity supply the per-axis building block; the 3D operator is their sum.
proof idea
Pure definition. At each site x and matrix entry (i,j), sum over a : Fin 3 the standard second-difference
N² · (H(x+e_a) − 2 H(x) + H(x−e_a))_{ij},
packaged via Matrix.of. No lemmas are applied; noncomputable only because the ambient complex/matrix infrastructure is.
why it matters
This is the flat positive operator that the whole axis-sector TT package rests on. Downstream, discLap3_planeH proves axis plane waves are eigenvectors with the same eigenvalue as the 1D mode (y,z stencils act trivially). That identity is packaged into discrete_tt_spectrum_converges_to_flat_lichnerowicz: discrete-transverse axis waves, exact eigenvectors at every N, and continuum limit of the discrete eigenvalue to the flat Lichnerowicz symbol.
In CurvedOperatorUnderdetermination it appears as the certified flat piece of curvatureCoupledOperator (−discLap3 plus a zeroth-order curvature coupling). The countermodel theorems discLap3_constantPlusField_zero and extensions_distinct_at_nonzero_curvature use that constants (plus polarization) lie in its kernel, so distinct curvature coefficients yield distinct operators. Framework role: first Lean bridge from lattice TT spectrum to continuum Lichnerowicz on flat T³, still axis-sector only pending the C10 isotropy probe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.