e_012113
plain-language theorem explainer
Case equality: the Regge midpoint numerator m2Num at multi-index (0,1,2,1,1,3) equals eight times the explicit kernel value explicitZ there. Gravity analysts cite it when assembling the full 4D identity m2Num = 8·explicitZ over (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(0,1,2,1,1,3)\in(\mathbb{F}_4)^6$, the integer numerator $m_2^{\mathrm{num}}(0,1,2,1,1,3)$ equals $8$ times the explicit kernel integer $Z(0,1,2,1,1,3)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification: it discharges a block of the pointwise claims $m_2^{\mathrm{num}}=8\cdot Z$ by kernel decision (module doc: "m2Num = 8·explicitZ, chunk 1 (256 kernel decides)").
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of coupling contributions over a fixed list couplingZList, summing contrib t a b c d i j into an Int. The comparison target explicitZ is a closed-form six-index integer table on Fin 4, with sparse nonzero entries such as $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$.
Indices run in Fin 4 (four discrete directions in the 4D simplex/edge labeling). The present declaration fixes one concrete sextuple $(0,1,2,1,1,3)$ inside that finite grid.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values (left via the fold definition of m2Num, right via the pattern-match table explicitZ scaled by 8), and Lean’s decision procedure checks integer equality. No lemmas beyond the two defining defs are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathbb{F}_4$, $m_2^{\mathrm{num}}=8\cdot Z$, by exhausting the finite index grid (downstream uses fin_cases on all six arguments). That global identity is the algebraic core of the Regge exact-midpoint $M_2$ TT certification in 4D gravity analysis inside the monolith.
In the broader Recognition Science gravity stack this is bookkeeping, not a new physical law: it locks the discrete curvature/coupling numerator to the explicit kernel so later continuum or continuum-limit arguments can quote a single closed form. It does not itself invoke the forcing chain (T5–T8), RCL, or the $\varphi$-ladder; those enter only if the certified kernel is wired into RS mass or ILG layers downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.