e_313310
plain-language theorem explainer
For the six-index tuple (3,1,3,3,1,0) in Fin 4, the folded numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity cite this as one of the 256 kernel cases. The proof is a single decide on concrete integer arithmetic.
Claim. For indices $a{=}3,\,b{=}1,\,c{=}3,\,d{=}3,\,i{=}1,\,j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(3,1,3,3,1,0)=8\,Z_{\mathrm{expl}}(3,1,3,3,1,0)$.
background
This module is chunk 13 of a 256-case kernel certification that the Regge midpoint numerator $m_2^{\mathrm{num}}$ coincides with eight times an explicit integer table $Z_{\mathrm{expl}}$ on all six-tuples in $(\mathrm{Fin},4)^6$.
The numerator is defined by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums the contribution of each coupling term at those indices. The explicit table $Z_{\mathrm{expl}}$ is a pattern-matched integer function on the same six indices (typical nonzero values are $\pm 2,,4$).
The local goal is purely arithmetic: evaluate both sides at one concrete multi-index and check equality in $\mathbb{Z}$.
proof idea
One-line kernel proof: by decide. Lean reduces both the fold that defines the numerator and the pattern match that defines the explicit table to concrete integers, then discharges equality by the decidable instance on Int. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases on all six indices, invoking one chunk lemma per cell. This identity is the algebraic core of the exact midpoint M2 TT certification in the 4D Regge gravity analysis: once every cell matches, the closed-form kernel may replace the folded sum in downstream curvature and mass identities. It is bookkeeping inside the gravity stack, not a forcing-chain (T0–T8) step, but it closes a concrete computational gap needed for exact rather than approximate midpoint identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.