e_310223
plain-language theorem explainer
Pointwise check that the Regge midpoint m2 numerator equals eight times the explicit Z kernel at multi-index (3,1,0,2,2,3). Gravity analysts assembling the 4D midpoint TT identity cite it as one of 256 kernel cells. The proof is a closed integer decision: both sides evaluate and match.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,2,2,3)$ 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 kernel $Z(a,b,c,d,i,j)$.
background
This module is one chunk of a 256-cell kernel certification that the midpoint Regge $m_2$ numerator coincides with eight times an explicit integer table $Z$ on all 4D multi-indices. The ambient setting is discrete gravity analysis: couplings on $\mathrm{Fin},4$ edges and faces are summed into a numerator that should match a closed-form kernel used in the TT midpoint identity.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and adding each contribution at the six indices. The companion $Z$ is an explicit case table $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample entries include $4$ on diagonal pairs such as $(0,0,1,1,2,2)$ and $-2$ on crossed pairs). The claim here is only the single cell $(3,1,0,2,2,3)$.
proof idea
One-line computational proof: decide evaluates both integer sides of the equality after unfolding the fold-definition of the numerator and the case table for $Z$ at this fixed six-tuple, then checks numeral equality. No lemmas beyond kernel definitions are required.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on each $\mathrm{Fin},4$ coordinate; this declaration discharges the cell $(3,1,0,2,2,3)$ inside that case tree (chunk 13 of the 256 decides). In the gravity stack it underwrites the exact midpoint TT identity in 4D Regge analysis, so the continuum-facing curvature bookkeeping can quote a fully certified discrete kernel rather than a schematic factor of eight. It does not itself invoke the RS forcing chain (T5–T8) or the RCL; it is pure discrete-kernel arithmetic supporting the gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.