e_033301
plain-language theorem explainer
For the concrete Fin-4 multi-index (0,3,3,3,0,1), the folded Regge coupling numerator equals eight times the tabulated explicit kernel value. Gravity analysts cite it as one atomic case in the 4D midpoint M2 TT identity. The proof is a single kernel decide on closed integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,3,0,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit kernel entry: $m_2^{\mathrm{num}}(0,3,3,3,0,1)=8\,Z_{\mathrm{expl}}(0,3,3,3,0,1)$.
background
This module is chunk 3 of a 256-case kernel certification that the 4D Regge midpoint M2 numerator equals eight times an explicit integer table. The ambient setting is discrete gravity analysis: couplings on Fin-4 index sextuples arising from a midpoint TT identity.
The numerator m2Num is defined by folding a fixed coupling list and summing a local contribution at each tuple $(a,b,c,d,i,j)$. The comparison table explicitZ is a pattern-matched integer function on the same six Fin-4 arguments (typical nonzero values include $\pm 2,,4$). The claim is the pointwise equality of these two integers at one fixed multi-index.
proof idea
One-line closed decision: both sides evaluate to concrete Int values (fold of a finite list versus a pattern match), so decide discharges the equality with no lemmas or case splits beyond the kernel.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every Fin-4 sextuple by exhaustive fin_cases. That global equality is the certified algebraic content of the ReggeExact midpoint M2 TT identity in 4D: the folded numerator is identically eight times the explicit kernel. This chunk case is one of the 256 atomic decides that close the certification; without it the assemble proof cannot cover the full index space. It sits in the Gravity analysis layer supporting discrete curvature bookkeeping, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.