e_302111
plain-language theorem explainer
For the six-index tuple (3,0,2,1,1,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts cite it as one cell of the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,0,2,1,1,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator $m_2$ is defined by folding a fixed coupling list: start at 0 and add each term's contribution at the given indices. The companion map explicitZ is a sparse case table of small integers (entries such as $4$, $-2$, and so on) that is meant to be the closed form of that fold, up to a universal factor of 8.
This module is chunk 12 of a 256-cell kernel certification: each cell fixes one concrete six-tuple and asserts $m_2=8Z$ there. The local setting is pure finite enumeration over $\mathrm{Fin},4$, with no continuum limit or curvature hypothesis yet.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left by evaluating the fold of couplingZList contributions at $(3,0,2,1,1,1)$, the right by looking up explicitZ at the same indices and multiplying by 8. The kernel checks integer equality.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $\mathrm{Fin},4$ by exhaustive fin_cases. That global equality is the algebraic core of the Regge exact midpoint $M_2$ TT identity in 4D gravity analysis inside the monolith. Without each chunk cell (including this one), the case split cannot close. The result is bookkeeping for a discrete curvature identity, not a continuum Einstein equation; it sits downstream of the kernel certificate definitions and upstream of the assembled forall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.