e_300020
plain-language theorem explainer
For the concrete Fin-4 multi-index (3,0,0,0,2,0), the folded numerator coupling m2Num equals eight times the explicit kernel table explicitZ. Gravity analysts cite it as one cell of the 256-case kernel identity. The proof is a single decide on the two integer values.
Claim. For indices $a=3$, $b=0$, $c=0$, $d=0$, $i=2$, $j=0$ in $\mathrm{Fin}\,4$, the numerator coupling satisfies $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8\,Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
This module is chunk 12 of a 256-cell kernel certification that the Regge midpoint numerator coupling equals eight times an explicit integer table on every sextuple of Fin-4 indices.
The numerator side is m2Num: it folds couplingZList, accumulating each term's contribution at the six indices. The closed form is explicitZ, a pattern-matched table Fin 4^6 → ℤ with sparse nonzero entries (e.g. 4 on diagonal-like pairs, −2 on crossed pairs).
The local claim is one concrete cell of that table identity, here at (3,0,0,0,2,0).
proof idea
One-line computational proof: decide evaluates both sides as concrete integers (the fold of m2Num at these indices versus 8 * explicitZ at the same indices) and checks equality in Int. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which states ∀(a b c d i j : Fin 4), m2Num = 8 · explicitZ by exhausting all sextuples with nested fin_cases. Each chunk theorem such as this one discharges one branch of that case split.
In the Recognition gravity stack this kernel identity is bookkeeping for the exact midpoint Regge/TT analysis in 4D: it certifies that the folded coupling numerator matches the hand-written sparse table used downstream. It does not itself touch T0–T8 or the J-cost forcing chain; it is pure discrete-kernel algebra inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.