e_020322
plain-language theorem explainer
Pointwise kernel identity: the folded m2 numerator at multi-index (0,2,0,3,2,2) equals eight times the explicit Z-table value there. Gravity analysts cite it when assembling the full 4^6 midpoint mass-squared identity. The proof is a single decide on concrete integer arithmetic.
Claim. At indices $(a,b,c,d,i,j)=(0,2,0,3,2,2)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
In the Regge exact-midpoint 4D analysis, two integer kernels are compared pointwise on $(\mathrm{Fin},4)^6$. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison table $Z$ is an explicit pattern-matched function $\mathrm{Fin},4^6\to\mathbb{Z}$ with sparse nonzero entries (e.g. $4$, $-2$ on selected index patterns).
This module is chunk 2 of the 256-case decide kernel that certifies $m_2^{\mathrm{num}}=8Z$ at every multi-index. The local setting is pure finite enumeration: no continuum limit and no floating-point residual.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(0,2,0,3,2,2)$. The left side runs the fold that defines the numerator; the right side looks up (or defaults) the explicit $Z$ entry and multiplies by $8$. Equality of the resulting integers is discharged by the kernel decision procedure.
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 chunk lemma such as this one closes one concrete cell of that $4^6$ grid. In the broader gravity stack the identity is the algebraic backbone of the Regge midpoint mass-squared TT kernel in 4D, so the continuum or continuum-limit claims downstream inherit a fully certified discrete numerator. It does not itself touch the RS forcing chain (T5–T8) or the J-cost; it is infrastructure inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.