e_312310
plain-language theorem explainer
For the six-index tuple (3,1,2,3,1,0) in (Fin 4)^6, the folded numerator m2Num equals eight times the closed-form table value explicitZ. Gravity analysts assembling the exact midpoint M2–TT identity cite this as one of the 256 kernel cases. The proof is a single kernel decide after unfolding both sides to integers.
Claim. For indices $a{=}3,\,b{=}1,\,c{=}2,\,d{=}3,\,i{=}1,\,j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(3,1,2,3,1,0)=8\,Z_{\mathrm{explicit}}(3,1,2,3,1,0)$.
background
The module sits in the Gravity analysis stack for the Regge exact-midpoint M2–TT identity in 4D. Local setting (module doc): prove $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$ by chunked kernel decides; this file is chunk 13 of that 256-case split.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at those six Fin-4 indices. The companion $Z_{\mathrm{explicit}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern table (sample entries: $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$, and so on).
The claim is the single-point instance of that table identity at $(3,1,2,3,1,0)$. Upstream, both sides are pure integer defs with no analytic hypotheses.
proof idea
One-line kernel proof: by decide. Lean unfolds m2Num (the fold over couplingZList of contrib) and explicitZ at the concrete Fin-4 sextuple, reduces both sides to closed integers, and checks equality by the decidable instance on Int. No lemmas beyond the two defs; no case split inside this declaration.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ in the assemble module, which states $\forall(a,b,c,d,i,j:\mathrm{Fin},4),,m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and discharges the quantifier by six nested fin_cases. Each leaf is one of these chunk theorems; this entry covers the $(3,1,2,3,1,0)$ leaf.
In the broader RS gravity stack, the identity certifies that the midpoint-discretized M2 numerator matches the explicit curvature/coupling table used in the 4D Regge analysis. It is pure discrete algebra (Fin-4 indices, integer fold), not a continuum GR derivation, and does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law. Its role is mechanical completeness: without every chunk leaf, the universal assemble theorem fails to close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.