e_012102
plain-language theorem explainer
For the six Fin-4 indices (0,1,2,1,0,2), the midpoint Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one cell of the 4D kernel identity table. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0,\,b{=}1,\,c{=}2,\,d{=}1,\,i{=}0,\,j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is obtained by folding a fixed coupling list: each term contributes an integer contrib at six simplex indices drawn from $\mathrm{Fin},4$, and the fold starts at $0$. The companion map explicitZ is a piecewise integer table on the same six indices (typical nonzero values $\pm 2,,4$).
The local module is chunk 1 of the identity $m_2^{\mathrm{num}}=8\cdot Z$: it discharges 256 concrete kernel cells by decide, rather than a symbolic argument. The full universal statement is assembled downstream by exhaustive fin_cases over all six indices.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values for the fixed sextuple $(0,1,2,1,0,2)$, so the equality is a decidable integer comparison with no lemmas beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z$ by casing every index and invoking the chunk cells. That global identity is part of the exact midpoint $M_2$ TT kernel certification in the Regge gravity stack: it replaces a symbolic sum over couplings by an eightfold multiple of a sparse closed-form table. Within Recognition Science gravity work this is bookkeeping infrastructure for the discrete curvature side, not a forcing-chain step (T0–T8), but it keeps the 4D kernel certificate fully computational and sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.