e_310232
plain-language theorem explainer
For the six Fin-4 indices (3,1,0,2,3,2), the folded numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts cite it when assembling the full 4D Regge midpoint M2TT identity over the 256-kernel. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3,b{=}1,c{=}0,d{=}2,i{=}3,j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(3,1,0,2,3,2)=8\,Z_{\mathrm{explicit}}(3,1,0,2,3,2)$.
background
In the 4D Regge midpoint analysis, the numerator m2Num is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The companion table explicitZ is a pattern-matched integer function on six Fin 4 arguments (sample values include 4, -2, and so on for the listed index patterns).
This module is chunk 13 of the 256-kernel decide campaign whose local claim is the pointwise identity m2Num = 8·explicitZ. The surrounding kernel-cert module supplies both definitions; the present file only discharges one concrete sextuple.
proof idea
One-line decide. Both sides reduce to concrete Int values for the fixed indices (3,1,0,2,3,2), so the kernel closes the equality with no lemmas or case splits.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the universal identity for all six Fin 4 arguments and proves it by exhaustive fin_cases. Each chunk theorem such as this one is a leaf of that case tree (or an equivalent decide leaf). The identity is infrastructure for the exact midpoint M2TT analysis in the Gravity domain; it does not itself invoke the T0–T8 forcing chain or the Recognition Composition Law, but sits under the discrete geometric layer those landmarks eventually constrain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.