e_310023
plain-language theorem explainer
For the six-index combination (3,1,0,0,2,3) on Fin 4, the folded M2 numerator equals eight times the explicit integer kernel value. Gravity analysts cite it as one atomic cell of the 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}1$, $c{=}0$, $d{=}0$, $i{=}2$, $j{=}3$ in $\mathrm{Fin}\,4$, the M2 numerator (fold of coupling contributions) equals $8$ times the explicit integer kernel $Z$ at those indices.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The M2 numerator is the fold of a fixed coupling list: each term contributes an integer depending on the six indices, and the fold starts at zero. The explicit kernel $Z$ is a closed-form pattern-matched integer table on the same index domain (typical values $\pm 2$, $4$, and so on).
The local module is chunk 13 of a 256-cell decide grid: each cell asserts numerator $= 8\cdot Z$ at one concrete six-tuple. The factor eight is the global normalization relating the folded coupling sum to the tabulated kernel in the midpoint M2–TT identity.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values (the fold over the coupling list versus eight times the pattern-matched kernel entry), 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 every six-tuple by exhaustive fin_cases and discharges each cell with a chunk theorem of this form. That global equality is the algebraic core of the Regge exact midpoint M2–TT identity in 4D gravity analysis inside the monolith. It is bookkeeping, not a new physical law: it certifies that the folded coupling definition matches the explicit kernel used downstream in curvature and mass-side identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.