LatticeField
plain-language theorem explainer
A lattice field in D dimensions is a real-valued assignment to every site of the integer lattice ℤ^D. It is the ambient type for log-ratio perturbations in the continuum-limit program: neighbor costs, the lattice Laplacian, and the F-014 certificate all take such fields as input. The definition is a pure type synonym, no proof content.
Claim. For any dimension $D \in \mathbb{N}$, a lattice field is a map $f : \mathbb{Z}^D \to \mathbb{R}$. Equivalently, sites are indexed by $D$-tuples of integers and each site carries a real log-ratio perturbation $t(x)$.
background
Module F-014 (ContinuumLimit) shows how discrete J-cost dynamics on ℤ³ produce smooth continuum physics. The J-cost $J(\exp(t)) = \cosh(t) - 1$ has leading Taylor term $t^2/2$; quadratic costs on a lattice yield the discrete Laplacian, which scales to $\nabla^2$ and thence to Klein-Gordon structure.
A lattice field is the carrier of those log-ratio perturbations: each site $x \in \mathbb{Z}^D$ holds a real value $t(x)$. Dimension $D$ is the free parameter here; elsewhere in the stack it is forced to $3$ (T8 / AlphaDerivation). Downstream objects (shifts along axes, neighbor J-cost sums, lattice Laplacian) are all typed over this synonym.
The module imports Cost, DiscretenessForcing, VariationalDynamics, and DimensionForcing, so the field type sits at the interface between the discrete ledger and continuum PDE language.
proof idea
Pure definitional synonym: LatticeField D is definitionally equal to (Fin D → ℤ) → ℝ. No tactics, no lemmas. Sites are functions from a finite coordinate basis into ℤ; the field returns a real at each site.
why it matters
This type is the common domain for the continuum-limit chain. It feeds lattice_laplacian, neighbor_cost, jcost_gives_laplacian_structure (J-cost of nearest-neighbor differences reduces to the lattice Laplacian in the small-perturbation regime), linearity lemmas, and the F-014 certificate continuum_limit_certificate (quadratic leading order → Laplacian → continuous ∇² → Klein-Gordon).
Outside the module it appears in gravity continuum emergence (jcost_neighbor_is_laplacian) and CubicRegge convergence certificates. Without a uniform lattice-field type, the discrete-to-continuum bridge (registry F-014) cannot be stated. Landmark link: T8 forces D = 3 spatially; the definition keeps D parametric so the same Laplacian story applies before specializing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.