e_310110
plain-language theorem explainer
For the six-index slot (3,1,0,1,1,0) on Fin 4, the folded numerator coupling m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. At multi-index $(a,b,c,d,i,j)=(3,1,0,1,1,0)$ with each index in $\{0,1,2,3\}$, the folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the TT-sector mass-squared numerator is assembled by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums contrib terms over couplingZList. The companion explicitZ is a piecewise integer table on $(\mathrm{Fin},4)^6$ that records the closed-form kernel values (e.g. $4$, $-2$, and the remaining default cases).
This module is chunk 13 of the 256-case kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The local setting is pure finite enumeration: every index runs over a four-element type, so each concrete sextuple is a decidable integer identity.
proof idea
One-line decide proof. Both sides reduce to concrete Int values once the six Fin 4 arguments are substituted: the left via the fold definition of m2Num, the right via the pattern-match table for explicitZ. Lean’s kernel closes the equality with no lemmas beyond evaluation.
why it matters
Feeds the master assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the claim by fin_cases on all six indices, invoking one atomic equality per cell. This chunk (and its siblings) therefore close the numerator half of the exact midpoint M2–TT identity in 4D Regge calculus inside the Gravity analysis stack. No open scaffold remains for this cell; it is a finished kernel fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.