e_310201
plain-language theorem explainer
For the multi-index (3,1,0,2,0,1) on Fin 4, the folded numerator m2Num equals eight times the explicit Z kernel. Gravity analysts cite it as one cell of the 256-case exhaustion that certifies the 4D Regge midpoint M2 TT identity. The proof is a single kernel decide on integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,2,0,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8\,Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the TT-sector identity is reduced to an equality between a folded numerator and a closed-form kernel. The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of contrib over couplingZList, summing integer coupling contributions at a fixed multi-index in $(\mathrm{Fin},4)^6$. The comparison value $Z_{\mathrm{explicit}}$ is a piecewise integer table on the same six indices (typical entries $\pm 2,,4$, and zero off the listed patterns).
This module is chunk 13 of the 256 kernel-decide cells that discharge one sextuple at a time. The local claim is exactly the instance at $(3,1,0,2,0,1)$. Upstream, both sides are pure Int-valued defs with no analytic hypotheses: the fold definition of the numerator and the pattern-match table for the explicit kernel.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the integer equality (the fold of contributions versus eight times the table lookup at $(3,1,0,2,0,1)$) and closes by kernel decision. No lemmas beyond the two defs are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles all $4^6$ index cases by nested fin_cases, and each leaf is one of these chunk theorems. This cell supplies the $(3,1,0,2,0,1)$ branch so the universal statement $m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ holds on the full multi-index domain. That identity is the algebraic core of the Regge exact midpoint M2 TT certification in 4D gravity analysis inside the monolith. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete kernel bookkeeping supporting the continuum gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.