e_320312
plain-language theorem explainer
Finite kernel check: at indices (3,2,0,3,1,2) the Regge midpoint mass-squared numerator equals eight times the explicit Z coupling. Gravity analysts cite it only as one cell of the 4D identity grid. Proof is a single decide on concrete integers from the fold and the lookup table.
Claim. For the sextuple of indices $(a,b,c,d,i,j)=(3,2,0,3,1,2)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$–TT identity certification. The local claim is the pointwise equality $m_2^{\mathrm{num}}=8\cdot Z$ on a block of the $4^6$ index space (here chunk 14 of the 256 kernel decides).
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start from $0$ and add each term's contribution at those six $\mathrm{Fin},4$ indices. The comparison value $Z$ is an explicit integer table on the same six indices (sample entries include $4$, $-2$, and other small integers on the diagonal and off-diagonal patterns).
Both definitions live in the kernel certificate module imported here; the chunk theorems only evaluate them at concrete sextuples.
proof idea
One-line computational proof: decide. Lean reduces both sides at the closed indices $(3,2,0,3,1,2)$ to concrete integers (the fold of contributions versus eight times the table entry) and checks equality by the decision procedure. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem is the full assembly m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the quantifiers by exhaustive fin_cases on all six $\mathrm{Fin},4$ indices. Each chunk theorem such as this one supplies one concrete cell so the case split can close without re-running the fold in the assembler.
In the gravity analysis stack this identity is bookkeeping for the exact midpoint Regge $M_2$–TT kernel in 4D: it certifies that the summed coupling numerator matches the closed-form $Z$ table up to the universal factor $8$. It does not itself touch the RS forcing chain (T5–T8) or the $\phi$-ladder mass formula; it is infrastructure inside the discrete gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.