e_013201
plain-language theorem explainer
For the Fin-4 multi-index (0,1,3,2,0,1), the Regge midpoint numerator coupling equals eight times the explicit kernel integer. Gravity analysts cite it as one cell in the 4^6 case split that builds the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on the unfolded integer equality.
Claim. For $a=0$, $b=1$, $c=3$, $d=2$, $i=0$, $j=1$ in $\mathrm{Fin}\,4$, the midpoint numerator coupling satisfies $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8\,Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-way kernel-decide split proving $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$ on all $\mathrm{Fin},4$ sextuples in the 4D Regge exact-midpoint analysis.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: each term contributes an integer via a local contribution map, then the contributions are summed. The explicit kernel $Z_{\mathrm{explicit}}$ is a pattern-matched integer table on the same six indices (sample values include $4$, $-2$, and so on).
The local claim is one concrete cell of that table identity, with indices fixed to $(0,1,3,2,0,1)$.
proof idea
One-line proof by decide. After unfolding $m_2^{\mathrm{num}}$ (the fold over the coupling list) and $Z_{\mathrm{explicit}}$ (the pattern match on the six indices), both sides reduce to concrete integers; the kernel checks equality. No lemmas beyond definitional reduction are invoked.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ in the assemble module, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and discharges the universal quantifier by nested fin_cases on all six $\mathrm{Fin},4$ arguments. Each leaf is one of these chunk theorems (here e_013201).
In the gravity stack this identity certifies that the midpoint numerator coupling is exactly eight times the closed-form kernel, a bookkeeping step inside the 4D Regge exact-midpoint TT analysis. It does not itself touch the T0–T8 forcing chain or the J-cost; it is pure discrete kernel arithmetic supporting the continuum gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.