Site3
plain-language theorem explainer
The type of integer lattice points in three dimensions, read as sites of the flat 3-torus under periodic identification. Every discrete tensor field, divergence, and Laplacian in the Discrete Lichnerowicz file is indexed by this carrier. It is a one-line type synonym for the product of three integer lines; no proof content.
Claim. Write $\mathrm{Site}_3 := \mathbb{Z} \times \mathbb{Z} \times \mathbb{Z}$ for the set of three-dimensional lattice sites (periodic reading: the flat $3$-torus).
background
The Discrete Lichnerowicz module closes Lane 4 of the Seven-Gaps campaign: operator convergence from a lattice perturbation spectrum to the continuum Lichnerowicz operator on a flat $3$-torus background. 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 on $\mathbb{Z}$ and periodicity supplies the torus reading.
A $3$D site is therefore a triple of integers. Tensor fields are $3\times 3$ complex matrices at each site. Axis unit shifts act componentwise on the triple; the forward-difference divergence and the componentwise three-axis discrete Laplacian are defined by summing those shifts. All convergence statements in the file are restricted to the axis stencil sector (plane waves $k=(k,0,0)$), not full isotropic recovery of the Lichnerowicz symbol.
proof idea
Pure abbreviation: the carrier type is definitionally the Cartesian product $\mathbb{Z}\times\mathbb{Z}\times\mathbb{Z}$. No tactics, no lemmas.
why it matters
This carrier is the domain for every lattice operator and mode in the file. Downstream, the discrete divergence, the $3$D Laplacian eigenvector identity for axis plane waves, the packaged axis-sector TT spectrum convergence to flat Lichnerowicz, and the curvature-coupled countermodel operators in CurvedOperatorUnderdetermination all quantify over sites of this type. Without a shared site type, the discrete-to-continuum comparison and the underdetermination witnesses cannot even be stated. It sits inside the gravity Seven-Gaps operator-convergence lane; it does not itself touch T0–T8 or the RCL, but it is the geometric substrate those continuum limits are discretized on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.