e_120200
plain-language theorem explainer
The numerator mass-squared coupling at multi-index (1,2,0,2,0,0) equals eight times the explicit 4D midpoint kernel value there. Gravity analysts cite it when assembling the full Fin-4 identity m2Num = 8·explicitZ. The proof is a single kernel decide on two concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(1,2,0,2,0,0)$ on $\mathrm{Fin}\,4$, the folded numerator coupling satisfies $m_2^{\mathrm{num}}(1,2,0,2,0,0)=8\,Z_{\mathrm{explicit}}(1,2,0,2,0,0)$.
background
This module is chunk 6 of a 256-case kernel certification that the Regge midpoint numerator $m_2^{\mathrm{num}}$ equals eight times an explicit integer kernel $Z_{\mathrm{explicit}}$ on every sextuple of $\mathrm{Fin},4$ indices.
$m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at those indices. $Z_{\mathrm{explicit}}$ is a closed-form pattern match on the six indices, returning small integers such as $4$, $-2$, and so on for the nonzero support.
The local goal is only the single sextuple $(1,2,0,2,0,0)$; sibling theorems cover the other points in the same chunk.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values (the fold of m2Num at fixed indices versus eight times the matching clause of explicitZ), so the kernel discharges equality with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ by exhaustive fin_cases over the six indices and invocation of these pointwise chunks. That identity is the certified algebraic core of the 4D Regge exact-midpoint $M_2$ TT analysis in the Gravity domain: once every kernel point matches, the continuum-facing mass-squared numerator is interchangeable with the explicit eightfold kernel. No open scaffold remains on this point; it is a closed decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.