e_310113
plain-language theorem explainer
For the six Fin-4 indices (3,1,0,1,1,3), the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one cell of the 256-way case split that certifies the 4D Regge midpoint M2 TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3,\,b{=}1,\,c{=}0,\,d{=}1,\,i{=}1,\,j{=}3$ in $\mathrm{Fin}\,4$, the coupling fold $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\cdot Z^{\mathrm{expl}}(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer depending on six $\mathrm{Fin},4$ indices. The closed form $Z^{\mathrm{expl}}$ is a sparse pattern-matched integer table on the same six indices (typical nonzero values $\pm 2,,4$).
The local module is chunk 13 of a 256-cell kernel certificate: every concrete sextuple must satisfy $m_2^{\mathrm{num}}=8,Z^{\mathrm{expl}}$. The parent assembly theorem then recombines the cells by exhaustive fin_cases on all six arguments.
This sits inside the Gravity.Analysis layer that checks exact algebraic identities for the Regge midpoint discretization of the M2 TT sector, before those identities are fed into continuum or continuum-limit arguments.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values (the fold over couplingZList versus the pattern match in explicitZ at (3,1,0,1,1,3)), and the kernel decides equality. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by casing through all 256 cells, including this one. That global equality is the certified algebraic core of the 4D Regge exact-midpoint M2 TT identity in the Gravity analysis stack.
Within Recognition Science gravity work, such kernel certificates lock the discrete curvature/coupling bookkeeping before continuum or phenomenological claims are drawn. The module doc frames the whole file as one chunk of that 256-decide cover. No open scaffold remains here: the cell is fully decided.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.