e_100222
plain-language theorem explainer
For the six Fin-4 indices (1,0,0,2,2,2), the folded Regge numerator m2Num equals eight times the explicit midpoint kernel table entry. Gravity analysts assembling the 4D midpoint M2TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,0,0,2,2,2)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(1,0,0,2,2,2)=8\,Z_{\mathrm{explicit}}(1,0,0,2,2,2)$.
background
The ambient module is a chunk of the 4D Regge exact-midpoint M2TT identity: the claim that the folded numerator m2Num equals eight times a sparse explicit integer table explicitZ on every 6-tuple of Fin-4 indices (256 cells total; this file is chunk 4).
m2Num a b c d i j is defined by folding a fixed coupling list: start at 0 and add each term's contribution at those indices. explicitZ is a pattern-matched Int table on Fin-4^6 (nonzero only on a thin set of midpoint configurations, e.g. values 4, -2, ...).
The local setting is pure integer arithmetic on a finite discrete kernel; no continuum limit or metric signature is taken inside the chunk.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values (left via the fold definition of the numerator, right via the pattern match on explicitZ at (1,0,0,2,2,2)), and the kernel checks equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all Fin-4 indices and discharges the cases by exhaustive fin_cases. That universal equality is the algebraic core of the Regge exact-midpoint M2TT identity in 4D gravity analysis inside the monolith.
Within Recognition Science this sits in the gravity stack (discrete curvature / Regge calculus side), not on the T0–T8 forcing chain itself. It closes one cell of the 256-kernel decide grid so the assembled identity can be cited without residual case obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.