e_131122
plain-language theorem explainer
At multi-index (1,3,1,1,2,2) the folded Regge midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one of the 256 concrete kernel checks that assemble the global identity. The proof is a single kernel decide on fixed Fin-4 indices.
Claim. For indices $(a,b,c,d,i,j)=(1,3,1,1,2,2)$ 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 value $Z(a,b,c,d,i,j)$.
background
This module is chunk 7 of a 256-point kernel certification that the midpoint Regge mass-squared numerator matches eight times an explicit integer table. Indices run over $\mathbb{F}_4$ (four discrete directions in the 4D simplex bookkeeping).
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at the six-index slot. The comparison target $Z$ is an explicit pattern-matched integer function on the same six $\mathbb{F}_4$ arguments (typical values $\pm 2,,4$ on the listed support).
The local claim is the single point $(1,3,1,1,2,2)$ of the identity $m_2^{\mathrm{num}}=8Z$ that the assembly theorem later quantifies over all indices.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple. The left side reduces by unfolding the fold over the coupling list; the right side multiplies the pattern value of the explicit kernel by eight. No lemmas beyond kernel reduction 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}}=8Z$ by exhausting all Fin-4 cases. That global identity is the certified algebraic core of the 4D Regge exact-midpoint mass-squared / TT analysis in this gravity stack.
Within Recognition Science gravity work, such kernel equalities lock the discrete curvature bookkeeping before continuum or phenomenological limits are taken. This chunk does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure integer certification supporting the Regge side of the program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.