e_201331
plain-language theorem explainer
Pointwise identity: the folded M2 numerator at multi-index (2,0,1,3,3,1) equals eight times the explicit integer Z-kernel there. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite it as one of 256 kernel cells. The proof is a single kernel decision (`decide`) on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,3,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 8 of a 256-cell kernel certification that the 4D Regge midpoint $M_2$ numerator matches eight times a closed-form integer table. The ambient setting is discrete gravity analysis: exact algebraic identities for the midpoint $M_2$–TT coupling on a 4-index simplex lattice.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing each term's contribution at six $\mathrm{Fin},4$ indices. The comparison object $\mathrm{explicitZ}$ is a pattern-matched integer table on the same six indices (typical values $\pm 2,,4$, and sparse support).
Upstream, both maps live in the kernel certificate module; this chunk only discharges one concrete six-tuple rather than the universal quantifier.
proof idea
One-line computational proof: decide evaluates both sides as concrete Int values and checks equality. No lemmas are invoked beyond the reducible definitions of the folded numerator and the explicit $Z$ table at the fixed indices $(2,0,1,3,3,1)$.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ by exhausting all $(\mathrm{Fin},4)^6$ cells. That universal identity is the algebraic backbone of the exact midpoint $M_2$–TT relation in the 4D Regge analysis stack.
Within Recognition Science gravity work, such kernel equalities pin the discrete curvature/coupling bookkeeping before continuum or phenomenological limits are taken. This cell is not itself a forcing-chain step (T0–T8); it is infrastructure under the gravity side of the monolith, closing one of 256 decide obligations in chunk 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.