e_312133
plain-language theorem explainer
One kernel case of the midpoint M2-numerator identity: at Fin-4 indices (3,1,2,1,3,3), the folded coupling sum equals eight times the explicit Z table entry. Gravity analysts cite it inside the exhaustive assembly that proves the identity for every sextuple. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,1,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 integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-case kernel certification that the Regge midpoint M2 numerator agrees with an explicit integer table, up to the universal factor 8. Indices run over $\mathbb{F}_4$ (four discrete labels), matching the 4D simplex bookkeeping in the surrounding gravity analysis.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add a local contribution at each coupling triple for the six indices. The comparison target $Z$ is an explicit pattern-matched integer table on the same six $\mathbb{F}_4$ arguments (sample entries include $4$, $-2$, and other small integers on the diagonal and off-diagonal patterns).
The local claim is the single sextuple $(3,1,2,1,3,3)$. Sibling chunk theorems cover the other concrete points; together they feed the global identity.
proof idea
One-line kernel proof: decide. Both sides reduce to closed integer expressions once the six Fin-4 indices are substituted into the fold definition of $m_2^{\mathrm{num}}$ and the pattern table for $Z$. Lean’s decision procedure checks the resulting integer equality with no further lemmas.
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 exhausting all Fin-4 sextuples. That global identity is the certified algebraic core of the Regge exact-midpoint M2/TT analysis in 4D: it replaces a symbolic fold by a closed table, so later curvature and graviton-sector identities can quote a pure integer factor rather than re-expanding couplings.
Within Recognition Science gravity work this is bookkeeping infrastructure, not a forcing-chain step (T0–T8). It closes one discrete cell of the 256-case kernel so the midpoint identity is machine-checked rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.