e_210201
plain-language theorem explainer
Pointwise identity: the midpoint mass-squared numerator at multi-index (2,1,0,2,0,1) equals eight times the explicit integer Z-kernel there. Gravity analysts cite it when assembling the full 4D Regge midpoint M2 TT numerator identity over (Fin 4)^6. The proof is a single kernel decision (`decide`).
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,2,0,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 9 of a 256-case kernel certification that the 4D Regge midpoint mass-squared numerator matches eight times an explicit integer table. The ambient setting is discrete gravity analysis: couplings on a 4-index simplex lattice with values in Fin 4.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each multi-index $(a,b,c,d,i,j)$. The comparison object explicitZ is a closed-form integer table on the same six Fin 4 arguments (nonzero only on a sparse set of index patterns, e.g. values $4$, $-2$, and so on).
The global claim is $m_2^{\mathrm{num}}=8,Z$ at every multi-index. Because both sides are computable integers on a finite domain, the identity splits into 256 pointwise equalities, of which this declaration is one.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(2,1,0,2,0,1)$ and checks integer equality. No algebraic lemmas are invoked; the kernel reduces the folded sum defining the numerator and the pattern-match defining explicit $Z$ to numerals and compares them.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the universal quantifier by exhaustive fin_cases on all six Fin 4 indices. Each chunk theorem such as this one is a named witness for one cell of that case tree (module doc: "m2Num = 8·explicitZ, chunk 9 (256 kernel decides)").
In the broader Recognition gravity stack, the midpoint M2 TT identity is part of the discrete curvature/coupling bookkeeping that must hold exactly before continuum or phenomenological limits are taken. Closing the 256 kernel cells removes a scaffolding gap in the 4D Regge analysis path; it does not itself invoke the forcing chain (T5–T8) or the RCL, but it hardens a gravity-side algebraic identity those layers rely on when matching discrete action terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.