LatticeField3
plain-language theorem explainer
Specializes the general D-dimensional lattice field to three spatial dimensions: real-valued maps on ℤ³. Continuum-limit and lattice-gravity arguments that work at the forced spatial dimension D = 3 cite this type. The body is a one-line abbreviation of the parametric lattice-field type at D = 3.
Claim. A lattice field on $\mathbb{Z}^3$ is a map $f:\mathbb{Z}^3\to\mathbb{R}$ (equivalently, a function from sites indexed by $\mathrm{Fin}\,3\to\mathbb{Z}$ into the reals), each site carrying a real log-ratio perturbation.
background
The ambient module treats multi-dimensional lattice Laplacian convergence: it lifts the one-dimensional continuum-limit second-order result to the full spatial lattice. The structural fact is that on the product lattice $\mathbb{Z}\times\mathbb{Z}\times\mathbb{Z}$, the D-dimensional lattice Laplacian is the sum of D independent one-dimensional second-difference operators, one per axis.
Upstream, a lattice field on $\mathbb{Z}^D$ is defined as a map $(\mathrm{Fin},D\to\mathbb{Z})\to\mathbb{R}$. Each site carries a log-ratio perturbation $t(x)$. Specializing the dimension parameter to 3 produces the type used throughout the D = 3 Laplacian, scaled Laplacian, and J-cost neighbor estimates in this file.
In the Recognition forcing chain, T8 fixes spatial dimension D = 3, so the three-dimensional lattice is the unique spatial setting in which the continuum kinetic operator is required to match linearized gravity.
proof idea
One-line abbreviation: instantiate the parametric lattice-field type at dimension parameter 3. No tactics, no lemmas, and no proof obligations.
why it matters
This type is the carrier for every D = 3 statement in the module. Downstream it appears in the three-term decomposition of the lattice Laplacian, the scaled Laplacian $(1/a^2)$ times that operator (the object that converges to $\nabla^2$), the sign-preservation lemma for the scaled operator, the J-cost neighbor approximation on $\mathbb{Z}^3$ (D = 3 case of the continuum J-cost-to-Laplacian structure), and the bundled LatticeConvergenceCert structure.
Module context ties the lattice Laplacian to the kinetic term in the lattice action; its continuum limit is $\nabla^2$, which for metric perturbations yields the linearized Ricci piece $R_{\mu\nu}\sim\nabla^2 h_{\mu\nu}$ in harmonic gauge. The specialization therefore sits on the T8 (D = 3) landmark and on the gravity continuum-limit bridge from discrete Recognition cost to continuum curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.