areaAlong_zero
plain-language theorem explainer
At vanishing Bloch momentum the phased area functional on a hinge slot collapses to the plain weighted sum of edge-class coefficients of H. Anyone assembling the M2 slot-coefficient identity cites this evaluation. The proof is a one-line simp of the cosine expansion at zero.
Claim. For any $4\times 4$ matrix $H$, slot $s\in\{0,\ldots,23\}$, and triangle index $t\in\{0,\ldots,9\}$, the area functional along the symbol direction at momentum scale zero equals $\sum_{d} a_{s,t}(d)\,c_d(H)$, where $a_{s,t}(d)$ is the slot-area covariance ($1/4$ on the two matching difference masks, else $0$) and $c_d(H)$ is the edge-class coefficient of $H$.
background
This module closes the punctured continuum limit of the folded M2 symbol along the Bloch ray for axis-TT and pure-gauge polarizations in 4D Regge calculus. The area functional areaAlong is the phased class-dot of the slot-area covariance against the edge-class coefficients of a metric perturbation $H$, evaluated on the ray $\mu\cdot\mathrm{symbolDir}$ with hinge base phase.
The expansion areaAlong_eq writes that functional as $\sum_d a_{s,t}(d),c_d(H),\cos(\mu,\theta_d)$, where $c_d(H)=D^\top H D$ is the edge-class load and $\theta_d$ is the midpoint Bloch phase scale of class $d$. Slot-area covariance $a_{s,t}$ is supported only on the two difference masks of the hinge, each with weight $1/4$.
The shifted cost $H(x)=J(x)+1$ from the Recognition cost algebra is imported only as ambient notation; the present identity is purely trigonometric and stencil-algebraic.
proof idea
One-line wrapper. Unfold via areaAlong_eq to expose the cosine factors, then apply Real.cos_zero so every $\cos(0\cdot\theta_d)=1$ and the sum collapses to $\sum_d a_{s,t}(d),c_d(H)$.
why it matters
Feeds m2SlotCoeff_eq_area_kerM2, which identifies the M2 slot coefficient with the product of zero-momentum area and the M2 kernel coefficient on T11 hinges (and zero otherwise). That identity is a step toward closing FoldAlongM2Tendsto for axis-TT and pure-gauge polarizations, using the already-proved cosine two-jet continuum limit and zero-momentum vanishing of the deficit kernel on those sectors.
In the broader gravity analysis this supplies the $\mu=0$ area factor in the Bloch-folded second-moment symbol, so the punctured Tendsto along symbolDir can be reduced to kernel asymptotics. General $H$ outside the named axis/gauge polarizations remains a Prop from the symbol module; this lemma itself is unconditional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.