e_021012
plain-language theorem explainer
For the concrete Fin-4 indices (0,2,1,0,1,2), the folded midpoint numerator equals eight times the explicit kernel integer. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one cell of the 256-case kernel. The proof is a single computational decide on two closed integer expressions.
Claim. With indices $a=0$, $b=2$, $c=1$, $d=0$, $i=1$, $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 kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a brute-force certification that the 4D Regge midpoint numerator equals eight times a sparse explicit kernel on every sextuple of Fin-4 indices. The ambient setting is discrete gravity analysis: midpoint M2TT identities for Regge calculus in four dimensions.
The numerator m2Num is defined by folding a fixed coupling list and summing a local contribution at each tuple $(a,b,c,d,i,j)$. The comparison target explicitZ is a pattern-matched integer table on the same six Fin-4 arguments (typical nonzero entries are $\pm 2$ or $4$). The identity claimed cellwise is $m_2^{\mathrm{num}}=8\cdot Z$.
Upstream, both maps live in the kernel certificate module; this chunk only evaluates one fixed index cell.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin-4 indices are substituted, so the kernel equality checker discharges $m_2^{\mathrm{num}}(0,2,1,0,1,2)=8\cdot Z(0,2,1,0,1,2)$ with no manual algebra.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8\cdot Z$ by exhausting Fin-4 cases. This declaration is the cell for $(0,2,1,0,1,2)$ inside that assembly (chunk 2 of the 256 kernel decides).
In the Recognition gravity stack, the midpoint M2TT identity is bookkeeping infrastructure for discrete curvature and coupling numerics, not a forcing-chain landmark (T0–T8). It closes a finite certification obligation rather than an open analytic gap: once every cell matches, the folded numerator may be replaced by the sparse explicit table in downstream 4D Regge identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.