e_110231
plain-language theorem explainer
For the six-index tuple (1,1,0,2,3,1) on Fin 4, the folded numerator coupling m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts certifying the 4D Regge midpoint M2TT identity cite this as one atomic kernel cell. The proof is a single `decide` on concrete integers.
Claim. For indices $a=1,b=1,c=0,d=2,i=3,j=1$ in $\mathrm{Fin}\,4$, the numerator coupling $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
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator coupling $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing local contributions at those indices. The explicit kernel $Z$ is a sparse case table of small integers (entries such as $4$, $-2$, and so on) that is meant to match $m_2^{\mathrm{num}}$ up to a universal factor of eight.
This module is chunk 5 of a 256-cell kernel certification: each cell fixes one concrete six-tuple and checks the scalar identity by computation. The local setting is pure integer equality on a finite domain, not continuum GR.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(1,1,0,2,3,1)$ and confirms the integers agree. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (fold of contributions) and explicit $Z$ (case table).
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 six-tuple via nested fin_cases and needs each cell, including this one, to hold. That global identity is the algebraic backbone of the Regge exact midpoint M2TT certification in four dimensions: it says the folded numerator is exactly eight copies of the explicit kernel everywhere on the discrete index space. Within Recognition gravity analysis this is bookkeeping infrastructure for curvature/coupling identities, not a forcing-chain landmark (T5–T8), but it closes a finite kernel obligation the continuum story depends on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.