e_011202
plain-language theorem explainer
Pointwise check that the folded M2 numerator coupling equals eight times the explicit Z-table entry at multi-index (0,1,1,2,0,2) in Fin 4. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of 256 kernel cells. The proof is a single kernel decision on two concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}1$, $d{=}2$, $i{=}0$, $j{=}2$ in $\mathrm{Fin}\,4$, 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
In the 4D Regge exact-midpoint analysis, the M2 numerator is the integer obtained by folding a fixed coupling list: each term contributes an integer depending on six Fin-4 indices, and $m_2^{\mathrm{num}}$ is their sum. Parallel to that fold sits an explicit closed-form table $Z$ on the same six indices, with sparse nonzero values such as $\pm 2$ and $4$ on selected patterns.
The local module is chunk 1 of the 256 kernel decides establishing $m_2^{\mathrm{num}}=8\cdot Z$ cell by cell. Upstream, $m_2^{\mathrm{num}}$ is defined as that fold over couplingZList, while $Z$ is the pattern-matched integer table. The full quantified identity is assembled downstream by exhausting all Fin-4 sextuples.
proof idea
Both sides evaluate to concrete integers at the fixed sextuple $(0,1,1,2,0,2)$. The proof is the single tactic decide, which asks the kernel to confirm equality of those two computed Int values. No algebraic rewriting or case split appears at this leaf; the work is pure evaluation of the fold versus the table entry.
why it matters
This leaf is one cell in the 256-way partition that discharges $m_2^{\mathrm{num}}=8\cdot Z$ everywhere. The parent theorem m2Num_eq_eight_explicitZ introduces all six Fin-4 variables and runs fin_cases on each, routing every branch to a chunk equality of this form. That global identity is the algebraic core of the Regge exact-midpoint M2–TT certificate in 4D gravity analysis: it replaces the folded coupling sum by an eightfold multiple of a sparse explicit table, which is what later curvature and mass-squared identities consume. Within Recognition Science gravity work it is scaffolding for exact discrete identities rather than a continuum GR claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.