e_210323
plain-language theorem explainer
For the single multi-index (2,1,0,3,2,3) on Fin 4, the Regge midpoint mass-squared numerator equals eight times the explicit Z coupling. Gravity analysts cite it as one atomic case in the 4D kernel identity. The proof is a pure kernel decision (`decide`) with no algebraic rewriting.
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,3,2,3)$ in $\{0,1,2,3\}^6$, the integer midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit six-index coupling table.
background
This module is chunk 9 of a brute-force certification that the folded midpoint numerator equals eight times an explicit coupling table on every sextuple in $(\mathrm{Fin},4)^6$. The local slogan is "$m_2^{\mathrm{num}}=8\cdot Z$, 256 kernel decides per chunk."
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a contribution map over a fixed coupling list, accumulating an integer. The comparison target $Z$ is a closed-form pattern-matched table $\mathrm{Fin},4^6\to\mathbb{Z}$ (nonzero entries such as $4$ on diagonal-like pairs and $-2$ on crossed pairs).
The ambient setting is 4D Regge calculus at the exact midpoint: one wants a machine-checked identity between the assembled quadratic form numerator and a sparse explicit kernel, index by index.
proof idea
One-line computational proof: decide. Lean reduces both sides of the integer equality for the concrete sextuple $(2,1,0,3,2,3)$ and checks equality in the kernel. No lemmas are invoked beyond the evaluability of m2Num and explicitZ at closed Fin-4 literals.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal claim $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhausting Fin-4 cases; this declaration discharges one concrete cell of that grid (chunk 9). Without the cell-wise identities, the midpoint mass-squared kernel in 4D Regge analysis would remain an unchecked table equality.
In the broader Recognition gravity stack, such kernel certificates underwrite exact discrete curvature/mass identities before continuum or phenomenological limits are taken. The result is pure integer bookkeeping: it does not itself invoke the forcing chain (T0–T8), $\varphi$, or the eight-tick octave, but it hardens the 4D combinatorial substrate those layers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.