e_031003
plain-language theorem explainer
At multi-index (0,3,1,0,0,3), the Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it as one of the 256 concrete kernel checks that assemble into the global m2Num = 8·Z identity. The proof is a single kernel decide on fixed Fin-4 indices.
Claim. For indices $(a,b,c,d,i,j)=(0,3,1,0,0,3)$ with each entry in $\mathbb{F}_4$, the summed 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 sits in the 4D Regge exact-midpoint analysis. The object $m_2^{\mathrm{num}}$ is the integer obtained by folding a fixed coupling list: each term contributes an integer weight at a six-tuple of $\mathrm{Fin},4$ indices, and the fold starts from zero. The companion $Z$ is an explicit, pattern-matched integer table on the same six-tuple domain (typical nonzero values $\pm 2,,4$).
The local claim of the file is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$, discharged by 256 kernel decides split into chunks. Chunk 3 covers one block of those index combinations. Upstream, both $m_2^{\mathrm{num}}$ and $Z$ are defined in the kernel-certificate module that supplies the coupling list and the closed-form table.
proof idea
Pure computational discharge: decide evaluates both sides at the concrete six-tuple $(0,3,1,0,0,3)$. The left side runs the fold that defines the numerator; the right side looks up the matching clause of the explicit $Z$ table (or the default zero) and multiplies by eight. No lemmas are invoked beyond the decidable equality of the resulting integers.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies over all six $\mathrm{Fin},4$ indices and proves $m_2^{\mathrm{num}}=8\cdot Z$ everywhere by exhaustive fin_cases. Each chunk lemma such as this one supplies one concrete cell of that case tree, so the global identity is only as strong as the full set of decides.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge mass-squared kernel in 4D: it certifies that the summed coupling presentation agrees with the closed integer table used downstream. It does not itself touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder; it is infrastructure inside the gravity-analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.