sum_m2SlotCertZ_axis
plain-language theorem explainer
The double sum of integer m²-slot certificates for the axis TT+ coefficient vector, over all 24 hinge slots and 10 stencil types, equals −96. Gravity analysts cite it when extracting the closed-form small-momentum symbol of the (1,1) Bloch fold on the TT+ axis. The proof is a pure finite decidability check on an integer table.
Claim. Let $c$ be the integer coefficient vector of the axis TT+ mode. Summing the integer $m^2$-slot certificate of $c$ over all hinge slots $s\in\{0,\ldots,23\}$ and stencil types $t\in\{0,\ldots,9\}$ yields $-96$.
background
This module isolates the (1,1)-orbit contribution to the small-momentum ($m^2$) symbol of the 4D Regge Bloch fold blochFold11. It never redefines Hessians, kernels, or stencils; it only evaluates the fold along symbolDir = (1,1,0,0).
The certificate m2SlotCertZ c s t is the integer local contribution at slot $(s,t)$: if the pair is a T11-type hinge it returns $-A_0(c;s,t),K''(c;s,t)$, otherwise zero. The axis TT+ coefficient vector is the integer class covector with $+1$ on class bit 2 and $-1$ on class bit 3 (and zero elsewhere).
The double sum therefore assembles every nonzero T11 contribution of that mode into a single integer before any real scaling into the continuum $m^2$ symbol.
proof idea
The goal is an equality of two concrete integers: a finite double sum of values of a decidable integer-valued function versus the constant $-96$. After the definition of the certificate is unfolded, every summand is a closed integer expression in the fixed axis TT+ coefficients. Lean discharges the equality by decide (with raised recursion and heartbeat limits to traverse the $24\times 10$ table). No algebraic lemmas beyond decidable arithmetic are required.
why it matters
Downstream, m2Symbol_axisTTPlus rewrites the real $m^2$ symbol through the certificate equality and this sum, obtaining the closed value $-3$ for the axis TT+ mode. That value is one of the four landed claims of the module: the (1,1) fold is even, vanishes at zero on TT+ and gauge, and has $m^2$ coefficient $-3$ (TT, nonzero) versus $0$ (gauge).
In the broader Recognition gravity stack this is a concrete coefficient check inside the Regge–Bloch analysis that supports continuum recovery of the Einstein–Hilbert action; it does not itself close the open FoldAlongM2Tendsto glue or the global S_RS_converges_EH_4d / gap_action_recovery goals. It is the integer backbone of the TT+ half of the (1,1) symbol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.