e_312120
plain-language theorem explainer
At multi-index $(3,1,2,1,2,0)$ on $\mathrm{Fin}\,4$, the folded midpoint $M_2$ numerator equals eight times the explicit integer $Z$ table. Gravity analysts cite it as one of the 256 kernel point checks that assemble the global $m_2^{\mathrm{num}}=8Z$ identity. The proof is a single kernel `decide` on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,1,2,0)$ with each coordinate 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 table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ for the exact midpoint $M_2$ TT identity in 4D Regge analysis. Indices run over $\mathrm{Fin},4$ (four discrete directions).
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at the six indices. The companion $Z$ is an explicit integer table on the same six $\mathrm{Fin},4$ arguments (sample entries $4$, $-2$, and so on for distinguished patterns).
The local claim is only the single tuple $(3,1,2,1,2,0)$. Sibling theorems cover the other tuples in the same chunk style.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete integers once the six indices are fixed, so the equality is a closed numeric check with no algebraic rewriting or lemmas beyond the definitions of the folded numerator and the explicit $Z$ table.
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$ by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments and discharge of each point goal. Without the point identities, the global midpoint $M_2$ TT numerator identity in 4D does not close.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact discrete curvature/coupling identities behind the Regge midpoint analysis, not a forcing-chain (T0–T8) step. It touches no open scaffold: it is a finished kernel fact inside the 256-decide grid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.