e_222202
plain-language theorem explainer
For the multi-index (2,2,2,2,0,2) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it as one cell of the 4^6 case split that proves the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on concrete integers.
Claim. For $a=b=c=d=2$, $i=0$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(2,2,2,2,0,2)=8\,Z_{\mathrm{expl}}(2,2,2,2,0,2)$.
background
This module is chunk 10 of a brute-force certification that the Regge midpoint numerator m2Num equals eight times an explicit integer kernel explicitZ on every 6-tuple of indices in Fin 4 (256 decides per chunk).
m2Num a b c d i j folds a fixed coupling list, summing a contribution at each term. explicitZ is a closed-form pattern match on the same six Fin-4 arguments, returning small integers (e.g. 4, -2, …). The identity m2Num = 8 · explicitZ is the algebraic content being certified cell by cell.
The ambient setting is 4D Regge calculus at the exact midpoint: the numerator of a mass-squared / TT-mode identity is reduced to a finite integer table, then matched against the explicit kernel.
proof idea
One-line computational proof: by decide. Both sides are closed integer expressions once the six Fin-4 indices are substituted (left via the fold definition of m2Num, right via the pattern match of explicitZ), so the kernel decides equality of two concrete Int values. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all a b c d i j : Fin 4 by exhaustive fin_cases and dispatches each cell to a chunk lemma of this form. Without the full 4^6 grid of decides, the midpoint TT / mass-squared numerator identity in the 4D Regge analysis stays uncertified.
In the broader Recognition gravity stack this is pure scaffolding for an exact discrete identity, not a continuum GR claim. It does not itself invoke the forcing chain (T0–T8), phi, or the eight-tick octave; those enter only if the certified kernel is later tied to RS-native constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.