e_011232
plain-language theorem explainer
For the Fin-4 multi-index (0,1,1,2,3,2), the M₂ numerator coupling equals eight times the explicit Z table entry. Gravity analysts cite it as one atomic cell of the 4D Regge midpoint M₂–TT identity. The proof is a single kernel decide on two closed integer expressions.
Claim. For indices $(a,b,c,d,i,j)=(0,1,1,2,3,2)$ with each index in $\{0,1,2,3\}$, the folded M$_2$ numerator equals eight times the explicit integer $Z$-coefficient: $m_2^{\mathrm{num}}(0,1,1,2,3,2)=8\,Z_{\mathrm{expl}}(0,1,1,2,3,2)$.
background
The module is a chunk of the 4D Regge exact-midpoint analysis: it certifies the pointwise identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ on a block of the $4^6$ index space by kernel decision.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating integer contributions at those six Fin-4 slots. The explicit table $Z_{\mathrm{expl}}$ is a pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and so on for the listed patterns).
Upstream, both objects live in the kernel-certificate module; this chunk only evaluates one concrete sextuple.
proof idea
One-line proof: decide. Lean reduces both sides to concrete integers (the fold for the numerator versus eight times the matched table entry) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the two sides.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the full universal statement by fin_cases on all six indices; each chunk theorem such as this one discharges one cell of that case tree. The identity is the algebraic core of the Regge exact-midpoint M₂–TT certificate in four dimensions: once every cell matches, the numerator coupling is identically eight times the closed Z table, which is what the gravity analysis needs for the midpoint reduction. It is pure bookkeeping scaffolding inside the Gravity domain, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.