e_330203
plain-language theorem explainer
Single index-point identity: the Regge midpoint mass-squared numerator at multi-index (3,3,0,2,0,3) equals eight times the explicit integer kernel Z there. Gravity analysts cite it only as one of the 256 kernel decides that assemble the global m2Num = 8·Z statement. Proof is pure computation via decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,3,0,2,0,3)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 15 of a 256-way case split proving that the midpoint Regge mass-squared numerator coincides with eight times an explicit integer kernel on all of $(\mathrm{Fin},4)^6$. The local setting is pure discrete gravity bookkeeping: no continuum limit is taken here.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a contribution functional at the six indices. The comparison object $\mathrm{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern match (sample values include $4$, $-2$, and so on on the diagonal and off-diagonal blocks).
Upstream, both definitions live in the kernel-certificate module; this chunk only evaluates them at one concrete six-tuple.
proof idea
One-line computational proof: decide. After the six Fin-4 arguments are substituted, both sides reduce to concrete integers (the fold on the left, the pattern match on the right), and the kernel decides equality. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ in the assemble module, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z$ and discharges the universal quantifier by nested fin_cases, invoking one decide-lemma per cell. This declaration is the cell for indices $(3,3,0,2,0,3)$.
In the broader Recognition gravity stack the identity certifies that the discrete midpoint second-variation numerator is exactly eight copies of the closed-form kernel, a bookkeeping step toward the exact Regge/TT midpoint analysis. It does not itself touch the forcing chain (T0–T8), RCL, or continuum constants; it is infrastructure under the 4D kernel certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.