e_220320
plain-language theorem explainer
Pointwise check that the Regge midpoint mass-squared numerator equals eight times the explicit Z-kernel at multi-index (2,2,0,3,2,0). Gravity analysts cite it as one cell of the 256-case kernel identity. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. At indices $(a,b,c,d,i,j)=(2,2,0,3,2,0)\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 chunk 10 of a 256-cell case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on the 4D midpoint Regge kernel. Indices run over $\mathrm{Fin},4$, labeling discrete edge/face slots in the exact midpoint discretization.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contribution of each coupling term at the six indices. The comparison object $Z$ is an explicit integer table on $(\mathrm{Fin},4)^6$ (sparse closed form: values such as $4,-2,\ldots$ on selected patterns, zero elsewhere).
The local claim is only the single tuple $(2,2,0,3,2,0)$. Sibling chunk theorems cover the other tuples; the assemble theorem quantifies over all six indices.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are fixed, so the kernel evaluates the fold defining $m_2^{\mathrm{num}}$ and the pattern-match defining $Z$, then checks equality with the factor $8$. No lemmas beyond the two definitions are required.
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$ by exhausting all $\mathrm{Fin},4$ cases. That global identity is the algebraic backbone of the exact midpoint $M_2$ TT-channel analysis in the 4D Regge gravity stack: it replaces a summed coupling expression by a sparse closed-form kernel, enabling exact (not approximate) midpoint identities downstream.
Within Recognition Science gravity work, this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8). It does not touch $\phi$, the eight-tick octave, or the $\alpha$ band; it only certifies one discrete cell of the Regge kernel arithmetic used in the continuum-limit and continuum-matching arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.