e_013231
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at Fin-4 indices (0,1,3,2,3,1) equals eight times the explicit kernel Z at those indices. Gravity analysts cite it when assembling the full sextuple identity for the Regge exact-midpoint 4D mass-squared kernel. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,3,2,3,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-way split that certifies $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of $\mathrm{Fin},4$ indices for the Regge exact-midpoint 4D TT mass-squared kernel.
The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: it sums a local contribution over that list at the six indices. The explicit kernel $Z$ is a closed integer table on $(\mathrm{Fin},4)^6$ (sample values include $4$, $-2$, and so on for the listed patterns). Both live in the kernel-cert module imported here.
The local goal is purely algebraic bookkeeping: check one concrete sextuple so the assemble theorem can recombine all chunks into a universal identity.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,1,3,2,3,1)$ and checks integer equality. No lemmas beyond the definitions of the folded numerator and the explicit kernel table are required; the kernel reduces the closed integer expressions directly.
why it matters
Feeds the assemble theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ by exhausting all sextuples. That universal identity is the certified numerator half of the Regge exact-midpoint 4D TT mass-squared kernel used in the gravity analysis stack.
Within Recognition Science this is infrastructure for discrete curvature/mass-squared bookkeeping on the 4D index set, not a forcing-chain step (T5–T8) or an RCL identity. It closes one of 256 decide obligations so the assemble layer can quote a single clean equality rather than a raw fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.