e_312221
plain-language theorem explainer
Pointwise check that the Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z at multi-index (3,1,2,2,2,1). Gravity analysts cite it as one tile of the 256-case kernel identity. The proof is a single decide on concrete integers from the folded coupling list versus the closed-form table.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,2,2,1)$ with each index in $\mathbb{F}_4$, 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 13 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on all sextuples in $(\mathbb{F}_4)^6$. The setting is the exact midpoint analysis of a 4D Regge-type mass-squared identity used in the gravity sector.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the integer obtained by folding a fixed coupling list: each term contributes via a local contrib and the accumulator starts at 0. The comparison target explicitZ is a closed-form table $\mathbb{F}_4^6\to\mathbb{Z}$ with sparse nonzero entries (e.g. $4$, $-2$ on selected patterns).
The full identity is assembled downstream by exhausting all Fin-4 indices; each chunk theorem such as this one discharges one concrete sextuple so the assembly need only case-split and invoke the matching lemma.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six Fin-4 indices are fixed to 3,1,2,2,2,1. Lean reduces $m_2^{\mathrm{num}}$ by evaluating the fold over the coupling list and reduces $8\cdot Z$ by table lookup, then checks integer equality. No lemmas beyond the two definitions are required.
why it matters
Feeds the parent 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 six nested fin_cases over $\mathbb{F}_4$, dispatching each leaf to a chunk lemma of this form.
In the Recognition gravity stack, that global identity is the certified algebraic core of the exact midpoint M2/TT relation in 4D: it replaces a symbolic coupling sum by an explicit sparse integer kernel, enabling later curvature and continuum-limit arguments without residual summation. This declaration is pure scaffolding glue for that kernel certificate, not a physical law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.