LatticeTensorField
plain-language theorem explainer
A lattice tensor field assigns a complex 3×3 matrix to every integer site of the flat 3-torus. Spectral and gravity workers cite it as the domain type for discrete Lichnerowicz-style operators and for curved countermodel families built on them. The declaration is a pure type abbreviation: no proof obligations.
Claim. A lattice tensor field is a map from three-dimensional integer lattice sites $\mathbb{Z}^3$ (read periodically as the flat 3-torus) to complex $3\times 3$ matrices.
background
The module sits in the Seven-Gaps campaign, Lane 4 (operator convergence). It builds the first Lean link between discrete perturbation spectra on a lattice and the continuum Lichnerowicz operator, restricted to the flat 3-torus and to the axis-stencil sector only.
Sites are triples of integers $\mathbb{Z}\times\mathbb{Z}\times\mathbb{Z}$, interpreted as the flat 3-torus via axis-wise periodicity. Lattice functions are $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$ (spacing $h=1/N$), not functions on $\mathrm{ZMod},N$, so stencil identities hold pointwise without wraparound arithmetic.
A lattice tensor field is the natural tensor-valued upgrade: at each site one stores a full complex $3\times 3$ matrix. Downstream curved-operator work uses this type as the carrier for both the certified flat discrete Laplacian and for zeroth-order curvature couplings.
proof idea
Pure type abbreviation. It expands to the function type from three-integer lattice sites to complex $3\times 3$ matrices; there is no tactic or term proof.
why it matters
This type is the carrier for the discrete Lichnerowicz program on the flat 3-torus and for the curved underdetermination countermodels that sit on top of it. Downstream, CurvedOperatorUnderdetermination builds a one-parameter family of operators (flat axis Laplacian plus scalar curvature coupling) acting on lattice tensor fields, introduces constant plus-polarized test fields of this type, and proves that distinct curved extensions agree on the entire flat specialization yet differ at nonzero curvature. Those results feed the Gap-4 curvature-coupling blocker: flat spectrum alone does not fix the curved operator. The definition therefore anchors Lane 4 of the Seven-Gaps gravity campaign without claiming isotropic continuum recovery (axis-sector scope only).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.