e_103313
plain-language theorem explainer
Pointwise identity: the folded mass-squared numerator at multi-index (1,0,3,3,1,3) equals eight times the explicit Z-coupling at those same Fin-4 indices. Gravity analysts cite it as one cell of the 256-case kernel that rebuilds the global m2Num = 8·explicitZ identity. Proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,0,3,3,1,3)$ in $(\mathbb{F}_4)^6$, the folded coupling sum $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 4 of a 256-cell kernel certifying $m_2^{\mathrm{num}}=8\cdot Z$ for the exact midpoint Regge $M_2$ TT identity in 4D. Indices run over $\mathrm{Fin},4$, so there are $4^6=4096$ formal slots, but the cert is organized as decide-discharged pointwise equalities on the support that matters.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $\mathrm{explicitZ}$ is a closed integer table on six $\mathrm{Fin},4$ arguments (sample entries include $4$, $-2$, and sparse nonzero patterns on diagonal-like pairs).
Local setting is pure integer arithmetic on that table versus the fold; no continuum limit or variational argument is invoked here.
proof idea
One-line kernel discharge: by decide. Both sides evaluate to concrete Int values at the fixed tuple $(1,0,3,3,1,3)$, so the decision procedure compares the folded sum against $8$ times the matching explicitZ clause and closes the equality. No lemmas beyond the two definitions are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8\cdot Z$ and proves it by exhaustive fin_cases on all six indices, routing each leaf to a chunk equality of this form. Without the pointwise cells, the global algebraic identity behind the 4D midpoint Regge $M_2$ TT analysis does not close in Lean.
In the broader gravity stack this is bookkeeping infrastructure for the discrete curvature/mass-squared side, not a forcing-chain landmark (T5–T8) or an RCL identity. It exists so the certified kernel can be cited as a finished integer fact rather than a sorry-bearing table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.