e_210000
plain-language theorem explainer
Pointwise identity: the Regge midpoint mass-squared numerator at multi-index (2,1,0,0,0,0) equals eight times the explicit Z coupling there. Gravity analysts cite it as one of 256 kernel cells in the m2Num = 8·explicitZ certification. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,0,0,0)$ in $(\mathbb{F}_4)^6$, the integer mass-squared numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit coupling value $Z(a,b,c,d,i,j)$.
background
This module is chunk 9 of a 256-cell kernel certification that the midpoint Regge mass-squared numerator coincides with eight times an explicit integer coupling table on all of $(\mathbb{F}_4)^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contributions of each table entry at the six indices. The comparison target $\mathrm{explicitZ}$ is a closed-form integer table on the same six $\mathbb{F}_4$ arguments (sample values include $4$, $-2$, and so on for distinguished index patterns).
The local setting is pure finite enumeration: every index lives in $\mathrm{Fin},4$, so each cell is a concrete integer equality, not an analytic limit.
proof idea
One-line computational proof: decide evaluates both sides at the fixed tuple $(2,1,0,0,0,0)$ and checks integer equality. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (fold of contributions) and $\mathrm{explicitZ}$ (pattern-matched table).
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$ for all six indices, which exhausts $(\mathbb{F}_4)^6$ by nested fin_cases and discharges each cell with a chunk identity of this form. That global identity is the algebraic core of the 4D Regge exact-midpoint mass-squared / TT certification in the Gravity analysis stack. It is bookkeeping infrastructure for discrete curvature identities, not a continuum GR theorem and not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.