e_312020
plain-language theorem explainer
For the single multi-index (3,1,2,0,2,0) on Fin 4, the Regge midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D M2TT identity. The proof is a pure kernel decide on the folded coupling list versus the closed-form table.
Claim. For $a=3$, $b=1$, $c=2$, $d=0$, $i=2$, $j=0$ in $\mathrm{Fin}\,4$, the midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
This module is chunk 13 of the 256-case kernel certification that the Regge exact-midpoint numerator equals eight times a closed-form integer table on every sextuple of Fin 4 indices. The local slogan is $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: each term contributes an integer via a local contrib map, summed from zero. The companion $Z_{\mathrm{explicit}}$ is a pattern-matched Int table on Fin 4^6 (sample entries include 4 on diagonal-like pairs and -2 on crossed pairs).
The surrounding Gravity.Analysis development certifies an exact midpoint identity for the 4D Regge M2TT sector; each chunk discharges a block of concrete index tuples so the universal statement can be assembled by exhaustive fin_cases.
proof idea
One-line computational proof: by decide. Lean evaluates both sides on the concrete Fin 4 literals (3,1,2,0,2,0). The left side runs the fold that defines m2Num over couplingZList; the right side looks up (or reduces) 8 * explicitZ at the same indices. Equality of the resulting integers is decided in the kernel with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and proves it by nested fin_cases, invoking one atomic equality per sextuple. This chunk (and its siblings e_310000, ...) close the numerator side of the Regge exact-midpoint M2TT identity in 4D.
In the broader Recognition gravity stack, that identity is infrastructure for discrete curvature and midpoint-exact coupling bookkeeping; it is not itself a forcing-chain step (T5–T8), but it underwrites the discrete geometric layer those continuum limits sit on. No open scaffold remains on this particular index: the decide closes the case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.