kerAlong_axis_zero
plain-language theorem explainer
At zero Bloch momentum the deficit kernel along the plus transverse-traceless axis vanishes for every hinge-slot pair. Gravity analysts cite this when closing the continuum limit of the folded M2 symbol on that polarization. The proof is a two-line reduction: evaluate the kernel at μ=0, then invoke the already-proved class-dot vanishing on axis TT-plus.
Claim. For every hinge-slot pair $(s,t)$ with $s\in\{0,\ldots,23\}$ and $t\in\{0,\ldots,9\}$, the phased deficit kernel along the plus TT polarization $H_+=\mathrm{diag}(0,0,1,-1)$, evaluated at Bloch scale $\mu=0$, equals zero: $K_{H_+}(s,t;0)=0$.
background
The module closes the punctured continuum limit of the folded M2 symbol for two special polarizations: the plus transverse-traceless axis and pure gauge. The kernel along a fixed metric perturbation $H$ is
$$K_H(s,t;\mu)=\mathrm{phasedClassDot}(\mathrm{slotDeficitKer}{s,t},H,\mu\cdot\mathrm{symbolDir},\mathrm{hingeBase}{s,t}).$$
At $\mu=0$ the phase factors collapse and $K_H(s,t;0)$ reduces to the ordinary class-dot of the slot deficit kernel against the fifteen class coefficients of $H$.
The plus axis $H_+=\mathrm{diag}(0,0,1,-1)$ is the unnormalized TT polarization used throughout the 4D Regge-Bloch analysis. An upstream theorem already shows that this class-dot vanishes identically on $H_+$ for every slot-hinge pair, by integer reindexing of the kernel and the sign pattern of the axis coefficients.
proof idea
Term-mode, two steps. First rewrite with kerAlong_zero, which expands $K_H(s,t;0)$ to $\sum_d\mathrm{slotDeficitKer}_{s,t}(d),\mathrm{classCoeff}_H(d)$ (the cosine factors become 1). That sum is exactly classDot of the slot deficit kernel against $H$. Second, simpa with the definition of classDot discharges the goal by the upstream vanishing theorem classDot_slotDeficitKer_axis, specialized to the plus axis.
why it matters
This is the zero-momentum input required by FoldAlongM2Tendsto_of_axisTTPlus, which asserts the full folded-M2 continuum limit along the plus TT polarization. That parent theorem feeds the module goal of closing FoldAlongM2Tendsto for axis TT (and, separately, pure gauge). The module doc is explicit: general $H$ remains a named Prop from the symbol module; only these two polarizations are discharged. In the broader gravity stack the result is a concrete step toward matching the continuum graviton propagator from the discrete Regge-Bloch Hessian, without touching the Recognition forcing chain (T0-T8) or the mass ladder directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.