e_030311
plain-language theorem explainer
One of 256 concrete kernel equalities: the Regge midpoint mass-squared numerator at multi-index (0,3,0,3,1,1) equals eight times the explicit Z-coupling at the same indices. The assembly theorem that proves the identity for every Fin-4 sextuple cites these chunks. Proof is a single decide on a closed integer computation.
Claim. For the discrete multi-index $(a,b,c,d,i,j)=(0,3,0,3,1,1)$ on $\mathrm{Fin}\,4$, the mass-squared numerator $m_2^{\mathrm{num}}(0,3,0,3,1,1)$ equals $8\,Z(0,3,0,3,1,1)$, where $Z$ is the explicit integer coupling table and $m_2^{\mathrm{num}}$ is the fold of coupling contributions over the fixed coupling list.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The explicit coupling $Z(a,b,c,d,i,j)$ is a closed case table of small integers (entries such as $4$, $-2$, and so on). The mass-squared numerator $m_2^{\mathrm{num}}$ is defined by folding a contribution function over a fixed coupling list, starting from $0$.
The module is chunk 3 of a 256-way case split: every concrete sextuple is discharged separately so the global identity $m_2^{\mathrm{num}}=8Z$ can be assembled by exhaustive fin_cases. Local setting is pure integer arithmetic on those kernels; no continuum limit is taken here.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,3,0,3,1,1)$ and checks integer equality. The left side reduces by unfolding the fold-definition of $m_2^{\mathrm{num}}$; the right side multiplies the looked-up explicitZ entry by $8$. No lemmas beyond the two kernel definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,, m_2^{\mathrm{num}}=8Z$ and proves it by nested fin_cases over all six indices, each leaf a chunk equality of this form. That global identity is the algebraic core of the Regge exact midpoint $M^2$/$TT$ certificate in 4D gravity analysis inside the monolith. It does not itself touch T0–T8 or the RCL; it is infrastructure for the discrete curvature/mass kernel comparison used downstream in the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.