e_310132
plain-language theorem explainer
Pointwise identity: the Regge midpoint mass-squared numerator at multi-index (3,1,0,1,3,2) equals eight times the explicit kernel Z there. Gravity analysts cite it as one cell of the 4D midpoint M2–TT kernel certification. The proof is a single kernel `decide` on the integer equality after unfolding the fold and the explicit table.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,1,3,2)$ in $\{0,1,2,3\}^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel table.
background
In the 4D Regge midpoint analysis, the mass-squared numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at a six-tuple of face/edge indices in $\mathrm{Fin},4$. The companion table $Z$ is an explicit integer-valued kernel on the same six-tuples (pattern-matched cases such as $(0,0,1,1,2,2)\mapsto 4$ and off-diagonal sign patterns $\mapsto -2$).
This module is chunk 13 of a partitioned certification that $m_2^{\mathrm{num}}=8Z$ holds at every multi-index. The local setting is pure finite enumeration: each chunk discharges a block of the $4^6$ cells by kernel decision rather than by a closed algebraic rewrite.
proof idea
One-line kernel proof: decide evaluates both sides as concrete integers. The left side unfolds the fold over couplingZList with the contribution function at $(3,1,0,1,3,2)$; the right side looks up explicitZ at the same tuple and multiplies by 8. Equality of the resulting Int values is decided by the kernel.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and is proved by exhaustive fin_cases on all six indices, each case invoking one of these chunk lemmas. That universal identity is the algebraic backbone of the Regge exact midpoint M2–TT certification in 4D: it converts the folded coupling definition into the closed explicit kernel used downstream in the gravity analysis stack. It is bookkeeping inside the discrete curvature/mass-squared sector, not a new continuum Einstein equation, but without the cellwise match the midpoint identity does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.