e_030221
plain-language theorem explainer
For the six-index slot (0,3,0,2,2,1) on Fin 4, the midpoint Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one atomic decide cell in the 4D M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=0$, $b=3$, $c=0$, $d=2$, $i=2$, $j=1$ in $\mathrm{Fin}\,4$, the folded midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at six Fin-4 indices, and the fold accumulates those contributions from zero. The companion map explicitZ is a sparse closed-form table on the same six indices, returning small integers such as $4$, $-2$, and so on at the nonzero patterns.
This module is chunk 3 of a 256-cell kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The local setting is pure integer arithmetic on Fin 4; no continuum limit or physical units enter the decide cells themselves. Upstream, both sides of the equality are the kernel definitions imported from the KernelCert module.
proof idea
One-line decide proof. Both sides reduce to concrete Int values for the fixed indices $(0,3,0,2,2,1)$: the left via the fold definition of $m_2^{\mathrm{num}}$, the right via $8$ times the matching explicitZ clause (or zero if unmatched). Lean’s kernel decision procedure discharges the integer equality with no lemmas or case splits in this file.
why it matters
This cell is one of the 256 atomic equalities assembled by m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases. That global identity is the algebraic backbone of the exact midpoint M2TT certificate in the 4D Regge gravity analysis.
Within Recognition Science gravity work, such kernel identities underwrite discrete curvature bookkeeping before continuum or phenomenological layers. The chunking (here chunk 3) keeps each decide small and auditable. No forcing-chain landmark (T5–T8) is directly at stake; the result is infrastructure for the Regge side of the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.