rawCellStencilTerm
plain-language theorem explainer
Defines the elementary summand of the Regge TT raw cell stencil: the product of two plane-wave tetrahedron edge velocities (with the f-slot sqrt-edge factor unfolded) times the flat angle Jacobian on slots f,g. Cited by the A2 audit equality, the Bloch cosine-fold assembly, and the zero-momentum constant-block identity. Pure definitional expansion, no proof obligations.
Claim. For lattice period $N\ge 1$, edge-length data $E$, integer mode $m\in\mathbb{Z}^3$, periodic Freudenthal tetrahedron $\tau$, and ordered edge slots $f,g\in\{0,\ldots,5\}$, the raw triple stencil term is $$\frac{v_f(\tau;m)}{2\sqrt{a^*_f}}\, v_g(\tau;m)\, J_{\mathrm{flat}}(f,g),$$ where $v_\bullet$ is the plane-wave tetrahedron velocity at commensurate momentum $2\pi m/N$, $a^*_f$ is the local squared Freudenthal edge length of slot $f$, and $J_{\mathrm{flat}}$ is the flat Schlaefli angle Jacobian.
background
This module is the panel-locked C11 interface audit for Regge TT second variation on a periodic Freudenthal torus. Attempt 1 was rejected for wiring the audit objects definitionally to their targets; here the raw stencil is kept as an explicit triple sum so that equality with the A2 reduced value is a genuine finite-distribution theorem.
A PeriodicTet N N N is a pair (vertex, Fin 6) indexing one of the six Freudenthal tetrahedra in each cubic cell of the $N\times N\times N$ torus. The local squared-edge tuple freudenthalTetSqEdges assigns to each of the six slots the Cayley–Menger lengths (unit steps, face diagonals, body diagonal). The plane-wave tetrahedron velocity evaluates the linearized edge stretch of a Bloch mode at commensurate momentum $2\pi m/N$. The flat angle Jacobian is the algebraic Schlaefli summand divided by hinge area on the flat background, used by the directional kill in the TT gate.
The module deliberately imports only the flat second-variation stack; no ContinuumLimit or spike certificate is in scope. Gates A2-full, A3, and B remain open.
proof idea
Definitional abbreviation only. The body multiplies three factors already present upstream: plane-wave tet velocity at slot $f$, divided by $2\sqrt{a^*_f}$ (the unfolded flatSlotSqrtDeriv), times plane-wave tet velocity at slot $g$, times flatAngleJacobian f g. No tactics, no lemmas applied beyond name resolution of those three symbols and commensurateMomentum.
why it matters
This term is the atomic summand inside rawCellStencil, the literal $6\times 6\times 6$-shape triple sum that Gate A1 equates to the A2 reduced finite second variation (a2_reduced_eq_rawCellStencil). Downstream, neg_rawCellStencilTerm_eq rewrites one signed copy as a cell-independent triple weight times two phase-shifted cosines, which feeds the finite-assembly headline rawCellStencil_eq_rawCosineBlochFold (raw stencil equals the raw bucket cosine fold under doubled-frequency non-aliasing). The zero-momentum specialization rawCellStencil_zeroMomentum reduces the same term to the per-cell assembled constant block, the diagnostic that the stencil-only constant block does not vanish and that ContinuumLimit must take the cosine two-jet route after the hinge/diagonal block is connected.
In the broader RS gravity stack this sits inside the discrete Regge path to continuum TT modes on the eight-tick / $D=3$ lattice geometry; it does not itself touch T5–T8 or the RCL, but supplies the audited interface those continuum claims will consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.