e_121012
plain-language theorem explainer
Pointwise identity: the midpoint Regge mass-squared numerator at multi-index (1,2,1,0,1,2) equals eight times the explicit integer kernel Z at those same indices. Gravity analysts cite it as one cell of the 256-case kernel table. The proof is a single kernel decide on concrete Fin 4 values.
Claim. For indices $a{=}1,\,b{=}2,\,c{=}1,\,d{=}0,\,i{=}1,\,j{=}2$ in $\mathrm{Fin}\,4$, 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 6 of a 256-cell kernel certification that the midpoint Regge mass-squared numerator equals eight times an explicit integer table $Z$ on $(\mathrm{Fin},4)^6$. The local slogan is $m_2^{\mathrm{num}}=8\cdot Z$.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a contribution at each tuple $(a,b,c,d,i,j)$. The companion $Z$ is an explicit case table of small integers (entries such as $4$, $-2$, and so on) on the same six indices. Both live in the kernel-cert module imported here.
The ambient setting is 4D Regge-calculus analysis in the Recognition gravity stack: discrete curvature/mass-squared identities reduced to finite integer arithmetic on $\mathrm{Fin},4$ labels.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(1,2,1,0,1,2)$ and checks integer equality. No lemmas are invoked beyond the definitions of the folded numerator and the explicit $Z$ table; the kernel closes the ground instance directly.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhaustive fin_cases and dispatches each cell to a chunk theorem of this form. Without the pointwise cells, the universal midpoint $m_2$ numerator identity does not close.
In the Recognition gravity analysis path, that universal identity is bookkeeping for the exact midpoint Regge mass-squared structure in 4D (discrete curvature couplings reduced to an explicit integer kernel). It is infrastructure rather than a T0–T8 forcing step, but it is required before higher continuum or phenomenological gravity claims can rest on a fully certified discrete kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.