e_210320
plain-language theorem explainer
For the discrete index tuple (2,1,0,3,2,0), the midpoint Regge mass-squared numerator equals eight times the explicit integer kernel Z. Gravity analysts assembling the 4D TT midpoint identity cite this as one decided kernel cell in chunk 9. The proof is a single kernel `decide` on concrete integer arithmetic.
Claim. At indices $(a,b,c,d,i,j)=(2,1,0,3,2,0)$ in $(\mathrm{Fin}\,4)^6$, the mass-squared numerator equals $8$ times the explicit integer kernel value $Z$ at those same indices.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local goal, stated in the module header, is to discharge many concrete instances of $m_2^{\mathrm{num}}=8\cdot Z$ by kernel decision (chunk 9 of the 256-cell schedule).
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: it sums a contribution functional over that list and returns an integer. The comparison table $Z$ is an explicit pattern-match on six $\mathrm{Fin},4$ indices, returning small integers such as $4$, $-2$, and so on at the matched cells (and, by the surrounding cert, the values needed for the identity).
Both objects live in the kernel-cert module imported here. The present declaration fixes one concrete six-tuple and asserts the scalar identity at that point.
proof idea
One-line proof: decide. Both sides reduce to concrete integers once the six indices are literals, so the kernel closes the equality with no lemmas and no case split inside this file.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$. Its proof is a full fin_cases tree that bottoms out on chunk lemmas of this form. Without each cell, the universal TT midpoint numerator identity does not assemble.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact discrete curvature/mass-squared comparison in 4D Regge calculus at the midpoint scheme, not a new physical law. It supports the certified algebraic spine behind the continuum-facing gravity claims rather than the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.