e_311223
plain-language theorem explainer
For the concrete Fin-4 multi-index (3,1,1,2,2,3), the Regge midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one cell of the 256-case kernel identity. The proof is a single kernel decide on closed integer arithmetic.
Claim. With indices in $\mathrm{Fin}\,4$, $m_2^{\mathrm{num}}(3,1,1,2,2,3)=8\,Z_{\mathrm{explicit}}(3,1,1,2,2,3)$, where $m_2^{\mathrm{num}}$ is the folded coupling-list numerator and $Z_{\mathrm{explicit}}$ is the closed-form integer kernel.
background
This module is chunk 13 of a 256-case kernel certification that the Regge-exact midpoint numerator equals eight times an explicit integer table on every sextuple of $\mathrm{Fin},4$ indices.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a coupling list and summing local contributions at those indices. The companion table $Z_{\mathrm{explicit}}$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample clauses give values such as $4$, $-2$, etc.).
The local claim is only the single cell with arguments $(3,1,1,2,2,3)$; sibling theorems cover the other cells in the same chunk.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six indices are fixed, so the kernel equality checker discharges $m_2^{\mathrm{num}},3,1,1,2,2,3=8\cdot Z_{\mathrm{explicit}},3,1,1,2,2,3$ 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}}$ and proves it by exhaustive fin_cases on all six indices. Each chunk cell such as this one supplies (or matches) one decided branch of that cover.
In the gravity analysis stack this identity is the algebraic backbone of the Regge-exact midpoint $M_2$ TT kernel in 4D: once numerator and explicit table agree up to the universal factor 8, downstream curvature and mass-response identities can quote a closed form instead of a folded sum. It is pure discrete linear algebra on the coupling list, not a continuum GR derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.