e_011002
plain-language theorem explainer
Pointwise identity: the folded M2 numerator at multi-index (0,1,1,0,0,2) equals eight times the explicit Z-table value there. Gravity analysts cite it when assembling the full 4D Regge midpoint M2–TT kernel identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,1,0,0,2)$ in $\mathrm{Fin}\,4$, the folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: sum the local contributions of each coupling triple at the given multi-index. The companion table $Z$ is an explicit case-split function returning small integers (typically $\pm 2,\pm 4$, or $0$ off the listed patterns).
The module is chunk 1 of a 256-way kernel split: each chunk discharges a block of concrete index tuples so the global identity $m_2^{\mathrm{num}}=8Z$ can be assembled by exhaustive fin_cases without a single giant decide. Local setting is pure integer arithmetic on the discrete 4D index set; no continuum limit is taken here.
proof idea
One-line computational proof: decide evaluates both sides at the fixed six-tuple $(0,1,1,0,0,2)$. The left side runs the fold that defines $m_2^{\mathrm{num}}$; the right side looks up (or defaults) the explicit $Z$ entry and multiplies by 8. Equality of the resulting integers is decided in the kernel. No lemmas beyond the two definitions are invoked.
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 proves it by six nested fin_cases, each leaf a chunk identity of this form. That global equality is the algebraic core of the Regge exact-midpoint M2–TT identity certificate in 4D gravity analysis inside the monolith. It is bookkeeping infrastructure, not a forcing-chain step (T0–T8), but it locks the discrete curvature/mass-squared kernel used downstream in the gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.