e_322220
plain-language theorem explainer
The numerator mass-squared coupling at the concrete multi-index (3,2,2,2,2,0) equals eight times the explicit integer kernel Z at those same indices. Gravity analysts assembling the full 4D Regge midpoint M2–TT identity cite this as one of the 256 kernel cells. The proof is a single decide on fully concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,2,2,2,0)$ in $\{0,1,2,3\}^6$, the folded numerator coupling $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
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared cellwise. The numerator coupling $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each list contribution evaluated at $(a,b,c,d,i,j)$. The explicit kernel $Z$ is a pattern-matched integer table on the same six indices (typical nonzero entries are $\pm 2,\pm 4$).
The local module is chunk 14 of the 256-cell decide campaign whose module slogan is "$m_2^{\mathrm{num}}=8\cdot Z$". Each chunk discharges a block of concrete sextuples so the global identity can be assembled by exhaustive case split on Fin 4.
proof idea
One-line computational proof: both sides are closed integer terms once the six Fin-4 arguments are literals, so decide evaluates the fold that defines $m_2^{\mathrm{num}}$ and the pattern match that defines $Z$, then checks equality to $8Z$. No lemmas beyond the two kernel definitions are required.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and proves it by six nested fin_cases sweeps. That universal identity is the algebraic core of the 4D Regge midpoint M2–TT certificate: once every cell matches, the continuum TT structure is recovered from the discrete midpoint stencil. Within Recognition gravity this is pure kernel bookkeeping rather than a forcing-chain step (T0–T8), but it is required scaffolding for the discrete-to-continuum gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.