discDiv
plain-language theorem explainer
Defines the forward-difference discrete divergence of a 3×3 lattice tensor field on the flat 3-torus: at site x and free index b it sums N times the axis increments of the a-b components. Gravity and discrete-GR workers cite it as the lattice stand-in for ∇·h in the TT gauge. The body is a direct stencil sum over the three unit axes, scaled by resolution N.
Claim. For lattice resolution $N\in\mathbb{N}$ and a lattice tensor field $H$ (a $3\times 3$ complex matrix at each site $x\in\mathbb{Z}^3$), the discrete divergence is $(\mathrm{div}_N H)(x)_b = \sum_{a=0}^{2} N\bigl(H(x+e_a)_{ab}-H(x)_{ab}\bigr)$, where $e_a$ are the three axis unit vectors.
background
The module builds the discrete Lichnerowicz operator on the flat 3-torus as part of Seven-Gaps Lane 4 (operator convergence). Lattice sites are Site3 = ℤ × ℤ × ℤ with N-periodic interpretation; spacing is $h=1/N$. A lattice tensor field assigns a complex $3\times 3$ matrix to every site.
The continuum TT gauge condition $\partial^a h_{ab}=0$ becomes a forward-difference stencil here. The factor $N$ normalizes the difference quotient so that as $N\to\infty$ the stencil approaches the continuum derivative. Only axis unit steps enter: the construction is deliberately restricted to the axis-stencil sector flagged in the module doc (Freudenthal energy is anisotropic; axis stencils do not recover the full isotropic symbol).
Spatial dimension is fixed at $D=3$ throughout (T8), matching the three summands over Fin 3.
proof idea
Pure definition: the body is the pointwise sum $\sum_{a:\mathrm{Fin},3} N\cdot\bigl(H(x+e_a){a b}-H(x){a b}\bigr)$. No lemmas are applied; unitVec supplies the three axis increments. Downstream proofs (planeH_transverse) unfold this definition and simplify the three-term sum by periodicity and polarization hypotheses.
why it matters
Supplies the discrete divergence that makes TT transversality a literal Lean statement. Parent theorem planeH_transverse proves that axis plane waves with vanishing first polarization row are exactly discrete-transverse: discDiv N (planeH N k eps) x b = 0. That fact is packaged into discrete_tt_spectrum_converges_to_flat_lichnerowicz, the file's main AXIS-SECTOR convergence result linking the lattice TT spectrum to the flat Lichnerowicz operator.
In the Recognition framework this is scaffolding for gravity-side operator recovery on the forced $D=3$ background (T8), not a continuum GR claim. The module explicitly bars reading axis-sector results as isotropic flat-space recovery; the direction-resolved symbol remains under the C10 probe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.