e_122333
plain-language theorem explainer
At multi-index (1,2,2,3,3,3) the folded M2 numerator equals eight times the explicit integer table entry. Gravity analysts proving the 4D Regge midpoint M2TT kernel identity cite this as one of 256 concrete cases. The proof is a single kernel decide on fixed integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,2,3,3,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-case kernel certification that the 4D Regge midpoint mass-squared numerator equals eight times a closed-form integer table. Indices run over $\mathbb{F}_4$ (four discrete labels), six of them at a time.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the six indices. The explicit table $Z$ is a pattern-matched integer function on the same six indices (typical values $\pm 2,,4$, and so on).
The local claim is the equality at one concrete six-tuple. Upstream, both sides are pure definitions in the kernel certificate module; no analytic hypothesis is left open.
proof idea
One-line proof by decide. Both sides evaluate to concrete integers once the six Fin-4 arguments are fixed, so the kernel reduces the equality to true with no lemmas or case splits inside this declaration.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every six-index case into the universal identity $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$, by nested fin_cases that discharge each concrete chunk theorem of this form. Without the per-tuple facts, the assemble step has nothing to quote.
In the Recognition gravity stack this closes the algebraic kernel of the 4D Regge midpoint M2TT identity: the numerator side matches the explicit table used downstream in curvature and mass-ladder bookkeeping. It is pure discrete certification, not a continuum GR derivation, and sits under the Gravity analysis branch rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.