e_312000
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at multi-index (3,1,2,0,0,0) equals eight times the explicit integer kernel Z at those indices. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,0,0,0)$ in $(\mathbb{F}_4)^6$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel on six $\mathbb{F}_4$ arguments.
background
This module is chunk 13 of a 256-cell kernel certification that the 4D Regge exact-midpoint M2 numerator equals eight times an explicit integer table. Indices run over $\mathbb{F}_4$ (four values), six of them labeling the discrete coupling slot.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a contribution function over a fixed coupling list and summing integer terms. The companion table $Z$ is a pattern-matched integer function on the same six indices (typical values $\pm 2,,4$, and zero off the matched patterns).
The local goal is purely algebraic bookkeeping: check one concrete six-tuple so a later exhaustive fin_cases assembly can quote every cell.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(3,1,2,0,0,0)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of the folded numerator and the explicit kernel 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 six nested fin_cases over $\mathbb{F}_4$ and discharge of each cell. That global identity is the certified numerator half of the 4D Regge exact-midpoint M2–TT relation used in the gravity analysis stack.
Within Recognition Science this sits in the discrete gravity / Regge sector that supports continuum limits and curvature bookkeeping; it does not itself touch the T0–T8 forcing chain, $\varphi$-ladder masses, or $\alpha$, but it hardens the 4D kernel those continuum arguments rely on. Closing all 256 chunks removes scaffolding from the M2 numerator identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.