e_212312
plain-language theorem explainer
Single kernel identity: the folded M2 numerator at index sextuple (2,1,2,3,1,2) equals eight times the explicit integer table entry. Gravity analysts cite it only as one cell of the 4D Regge midpoint M2–TT check. The proof is a pure `decide` on concrete Fin-4 data.
Claim. For indices $a{=}2,b{=}1,c{=}2,d{=}3,i{=}1,j{=}2$ in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer lookup table on six $\mathbb{F}_4$ arguments.
background
In the 4D Regge exact-midpoint analysis, the M2 numerator is defined by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums the local contribution of each coupling term at those six $\mathbb{F}_4$ slots. The companion object $Z$ is an explicit integer-valued table on the same six indices (pattern-matched closed form, e.g. values in ${4,-2,\ldots}$).
The module is chunk 9 of a 256-way kernel split: every concrete sextuple is discharged separately so the global identity $m_2^{\mathrm{num}}=8Z$ can be reassembled by exhaustive fin_cases. Local setting is purely combinatorial integer arithmetic on $\mathrm{Fin},4$, not continuum GR.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel decision procedure closes the equality with no lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and $Z$.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by casing on all six indices and invoking the chunk cells. That global identity is the algebraic core of the Regge exact-midpoint M2–TT certificate in 4D gravity analysis inside the monolith. It does not itself touch the T0–T8 forcing chain; it is infrastructure for the discrete curvature/mass-squared side of the RS gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.