e_303011
plain-language theorem explainer
For the six Fin-4 indices (3,0,3,0,1,1), the folded m2 numerator equals eight times the explicit integer kernel entry. Gravity analysts assembling the full Regge midpoint M2=8Z identity cite this as one of the 256 decided cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=3$, $b=0$, $c=3$, $d=0$, $i=1$, $j=1$ in $\mathrm{Fin}\,4$, 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
In the Regge exact-midpoint analysis for the 4D M2 TT identity, two integer kernels are compared cellwise on $(\mathrm{Fin},4)^6$. The folded numerator $m_2^{\mathrm{num}}$ is defined by folding a coupling list: it sums a contribution function over every term in couplingZList. The explicit kernel $Z$ is a pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on).
The local module is chunk 12 of the 256-cell decide campaign whose module slogan is "$m_2^{\mathrm{num}}=8\cdot Z$". Each cell is an equality of two concrete integers once the six indices are fixed. Upstream, both $m_2^{\mathrm{num}}$ and $Z$ live in the kernel certificate module and are pure definitions with no proof content.
proof idea
One-line kernel proof: by decide. After substituting the six concrete Fin 4 values, both sides reduce to closed integer expressions (a fold of contributions versus a pattern match in the explicit table), and the decision procedure checks numerical equality. No lemmas beyond the two definitions are invoked.
why it matters
This cell is one brick in the exhaustive identity m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j:\mathrm{Fin},4,, m_2^{\mathrm{num}}=8Z$. That parent theorem proceeds by six nested fin_cases sweeps and therefore depends on every concrete cell, including this one. Closing the full identity certifies that the folded Regge midpoint numerator is exactly eight times the explicit kernel, a numerical checkpoint inside the 4D gravity analysis stack. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is pure discrete kernel bookkeeping for the Regge M2 sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.