rawCellStencil
plain-language theorem explainer
Defines the raw Regge TT cell stencil as a normalized triple sum over periodic tetrahedra and ordered slot pairs, with an overall minus sign matching the Schlaefli-reduced second variation. Gravity analysts cite it as the non-tautological audit target for Gate A1 and as the finite assembly head for cosine Bloch folds. The body is a pure definition: scale by 2/N^3 and negate the sum of raw cell-stencil terms.
Claim. For lattice size $N\ge 1$, edge-length data $E:(\mathrm{Fin}\,3)^2\to\mathbb{R}$, and integer Bloch mode $m:\mathrm{Fin}\,3\to\mathbb{Z}$, the raw cell stencil is $$\frac{2}{N^3}\Biggl(-\sum_{\tau}\sum_{f=0}^{5}\sum_{g=0}^{5} T_N(E,m;\tau,f,g)\Biggr),$$ where the sum runs over periodic tetrahedra $\tau$ on the $N\times N\times N$ torus and ordered slot pairs $(f,g)$, and $T_N$ is the raw per-cell stencil term.
background
This module is the panel-locked C11 interface audit for Regge transverse-traceless (TT) second variation on a periodic tetrahedral lattice. Attempt 1 was rejected for wiring the audit objects definitionally to their targets; here the raw stencil is kept as an independent literal expression.
The sum is over PeriodicTet N N N (cells of the $N^3$ torus) and two Fin 6 indices (ordered hinge/slot pairs on a tetrahedron). The inner term expands the flat-slot angle derivative sum and writes the flat-slot square-root derivative as plane-wave tet velocity over $2\sqrt{a^*}$. The prefactor $2/N^3$ and the overall minus sign follow the live A2 convention: the reduced second variation is the negative Schlaefli-reduced contraction.
$E$ supplies the six edge lengths (or squared lengths) of the reference cell; $m$ is the integer Bloch wavevector. The definition does not import ContinuumLimit or spike certificates; it only names the finite triple sum that later gates compare against.
proof idea
Definitional, not a proof. The right-hand side multiplies the constant $2/N^3$ by the negation of a triple finite sum: outer sum over periodic tetrahedra, then two sums over Fin 6 slot indices, each summand the sibling rawCellStencilTerm. No lemmas are applied; unfolding this def is the first step in the Gate A1 equality and in the zero-momentum specialization.
why it matters
Gate A1 of the C11 audit: a2_reduced_eq_rawCellStencil proves the A2 reduced finite Hamiltonian equals this triple sum by distributing the inner flat-slot angle-derivative sum, not by definitional aliasing. That equality is strictly stronger than the panel's optional $N$-bound premise; it holds for every $N$ with NeZero N.
Downstream, rawCellStencil_eq_rawCosineBlochFold (finite assembly headline) equates the stencil to the raw bucket cosine fold under doubled-frequency non-aliasing, and rawCellStencil_zeroMomentum identifies the $m=0$ value with twice the per-cell assembled constant block. The module status block still leaves Gate A2-full (rational bucket aggregation), Gate A3 (hinge-aware zero mode), and Gate B (spike convention bridge) open; the sympy diagnostic already shows the stencil-only constant block does not vanish, so ContinuumLimit must take the cosine two-jet route after the hinge/diagonal block is connected.
In the broader RS gravity stack this is the honest finite skeleton against which Bloch and continuum claims are checked, not a continuum or curvature theorem itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.