e_020030
plain-language theorem explainer
Single multi-index identity: the Regge midpoint mass-squared numerator at (0,2,0,0,3,0) equals eight times the explicit integer kernel Z at those indices. Gravity analysts cite it as one cell of the 4D kernel table. Proof is a pure `decide` on the closed integer definitions.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,0,3,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin 4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib, and the fold starts at 0. The comparison target explicitZ is a sparse case table of small integers (entries such as $4$, $-2$, and so on) on the same six-index domain.
This module is chunk 2 of a 256-way split of the kernel identity $m_2^{\mathrm{num}}=8\cdot Z$. The local setting is pure finite enumeration: every index runs over a four-element type, so each concrete sextuple is a closed arithmetic claim.
proof idea
One-line computational proof: decide evaluates both sides from the definitions of m2Num (fold of contrib over couplingZList) and explicitZ (pattern-match table) and checks integer equality at the fixed indices $(0,2,0,0,3,0)$. No lemmas beyond the kernel definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases. That global equality is the certified bridge between the folded coupling numerator and the closed-form kernel used in the Regge midpoint $M^2$ TT analysis. Within Recognition gravity work this is bookkeeping infrastructure, not a forcing-chain step: it locks one cell of the discrete curvature/mass-squared table so downstream continuum or continuum-limit arguments can quote a fully discharged finite identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.