e_320001
plain-language theorem explainer
For the six-index tuple (3,2,0,0,0,1) on Fin 4, the folded Regge coupling numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it as one cell of the 256-case certificate that the midpoint M2 TT numerator matches 8Z. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(3,2,0,0,0,1)=8\,Z(3,2,0,0,0,1)$, where $Z$ is the explicit integer kernel on six indices.
background
In the 4D Regge midpoint analysis, the M2 TT identity is checked by comparing a folded numerator built from coupling contributions against a closed-form integer kernel. The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of contrib over couplingZList at six Fin-4 indices. The comparison target is explicitZ, a piecewise integer table on the same six indices (typical values $\pm 2,\pm 4$, etc.).
This module is chunk 14 of that certificate: each declaration fixes one concrete six-tuple and asserts numerator equals eight times the explicit kernel entry. The local setting is pure finite enumeration over $(\mathrm{Fin},4)^6$, not continuum GR.
proof idea
One-line decide on the ground instance. Both sides reduce to concrete Int values (fold of the coupling list versus the matching explicitZ clause), so the kernel closes the equality with no lemmas or case splits beyond evaluation.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the universal claim by fin_cases on all six indices, invoking each chunk cell (including this one) as a ground fact. That identity is the algebraic backbone of the ReggeExact midpoint M2 TT certificate in 4D gravity analysis inside the monolith. It does not itself touch the RS forcing chain (T5–T8) or the J-cost; it is infrastructure for the discrete curvature/TT side of the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.