e_021313
plain-language theorem explainer
For the six-index slot (0,2,1,3,1,3) on Fin 4, the folded Regge midpoint numerator equals eight times the explicit kernel value. Gravity analysts cite it when assembling the global m2Num = 8·explicitZ identity over all 4^6 index tuples. The proof is a single kernel decide on concrete integers.
Claim. With $a,b,c,d,i,j\in\{0,1,2,3\}$ specialized to $(0,2,1,3,1,3)$, the midpoint numerator $m_2^{\mathrm{num}}(0,2,1,3,1,3)$ equals $8$ times the explicit integer kernel $Z(0,2,1,3,1,3)$.
background
In the 4D Regge midpoint analysis, the numerator m2Num is the fold of a fixed coupling list: each term contributes an integer depending on six Fin-4 indices (two edge pairs and a midpoint pair). The companion table explicitZ is a closed-form case table of those same integers, normalized so the identity m2Num = 8·explicitZ is expected pointwise.
This module is chunk 2 of the 256-case kernel certification: each declaration pins one concrete six-tuple. The local setting is pure integer arithmetic on Fin 4; no continuum limit or physical units enter here.
Upstream, m2Num is defined by folding contrib over couplingZList, and explicitZ supplies the target integers (e.g. ±2, 4 on the listed patterns).
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are literals, so the kernel compares the folded sum against 8 * explicitZ 0 2 1 3 1 3 and closes the equality with no lemmas beyond the definitions of m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies over all six Fin-4 indices and discharges the universal claim by fin_cases; each chunk lemma such as this one fills one branch of that case split. The identity is the algebraic core of the Regge exact-midpoint M2TT certification in the Gravity analysis stack: once every tuple satisfies m2Num = 8·explicitZ, the midpoint curvature numerator is replaced by the compact explicit kernel everywhere downstream.
It does not itself touch the RS forcing chain (T5–T8) or the J-cost; it is infrastructure inside the discrete gravity side of the monolith, ensuring the 4D midpoint identities are machine-checked rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.