e_021210
plain-language theorem explainer
Pointwise kernel identity: the midpoint numerator coupling at multi-index (0,2,1,2,1,0) equals eight times the explicit integer kernel Z at those indices. Gravity analysts cite it as one cell in the 4D Regge midpoint M2TT certification grid. The proof is a single kernel decide on concrete Fin-4 data.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,2,1,0)$ in $\mathrm{Fin}\,4$, 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
This module is chunk 2 of a 256-cell decide grid certifying $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of $\mathrm{Fin},4$ indices. The setting is the exact midpoint identity for the 4D Regge/TT mass-squared numerator used in the gravity analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: each term contributes an integer via a local contribution map, and the fold starts at $0$. The comparison object $Z$ is an explicit case-table $\mathrm{Fin},4^6\to\mathbb{Z}$ (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$, and so on).
The present cell fixes one concrete multi-index and asserts numerical equality of the two sides.
proof idea
One-line computational proof: decide evaluates both the folded numerator and the explicit table entry at the concrete indices $(0,2,1,2,1,0)$ and checks integer equality. No algebraic lemmas are invoked beyond the kernel definitions of the fold and the case table.
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$ and discharges the universal claim by fin_cases on all six indices, each case pointing at a chunk cell such as this one.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2TT kernel in 4D: once every cell matches, the closed-form $Z$ may replace the folded coupling list in downstream curvature/mass-squared identities. It does not itself invoke the T0–T8 forcing chain, $\phi$-ladder masses, or the RCL; it is pure discrete kernel certification supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.