e_012322
plain-language theorem explainer
Pointwise kernel check: the folded coupling numerator at multi-index (0,1,2,3,2,2) equals eight times the explicit integer table at that same index. Gravity analysts cite it as one cell of the 4D Regge midpoint M2 numerator identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,2,3,2,2)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge exact-midpoint analysis for the M2 TT identity. The local goal, stated in the module header, is to certify $m_2^{\mathrm{num}}=8\cdot Z$ by 256 kernel decides, chunked across files.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six $\mathrm{Fin},4$ indices. The comparison object $Z$ is an explicit integer-valued table on the same six indices (pattern-matched closed form, with entries such as $4$, $-2$, and so on).
Both definitions live in the kernel certificate module imported here. The present declaration is one concrete cell of that table equality, for the multi-index $(0,1,2,3,2,2)$.
proof idea
One-line computational proof: decide. Lean reduces both sides at the fixed indices $(0,1,2,3,2,2)$ to concrete integers (the fold for the numerator versus eight times the table lookup) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all six $\mathrm{Fin},4$ indices, which exhausts cases and packages every cell of the identity. That global equality is the algebraic backbone of the 4D Regge exact-midpoint M2 TT certificate in the Gravity analysis stack.
Within Recognition Science gravity work, such exact discrete identities pin the curvature/coupling bookkeeping before continuum or phenomenological claims. This cell does not itself touch the forcing chain (T0–T8), the J-cost, or the $\varphi$-ladder; it is pure integer kernel support for the Regge side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.