e_220131
plain-language theorem explainer
For the multi-index (2,2,0,1,3,1) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel table entry explicitZ. Gravity analysts cite it as one cell of the 4D Regge midpoint M2 identity. The proof is a single decide on concrete integers.
Claim. For indices $a=2$, $b=2$, $c=0$, $d=1$, $i=3$, $j=1$ in $\{0,1,2,3\}$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 10 of a 256-cell kernel certification that the folded numerator of the 4D Regge exact-midpoint $M_2$ tensor equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$ (four spacetime directions).
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a coupling list and summing local contributions at those six indices. The companion table $Z$ is an explicit pattern-matched $\mathrm{Int}$-valued function on the same domain (nonzero only on a short list of index patterns such as $(0,0,1,1,2,2)\mapsto 4$).
The local claim is one concrete sextuple in that table identity, not the universal statement.
proof idea
One-line computational proof: decide evaluates both sides at the fixed Fin 4 constants and checks integer equality. No lemmas are invoked beyond the definitions of the numerator fold and the explicit kernel table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the universal quantifier by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each chunk cell such as this one is a leaf of that case tree.
In the gravity analysis stack this identity is the algebraic certificate that the midpoint Regge $M_2$ numerator matches the closed-form kernel used downstream. It is pure discrete linear algebra on the 4D index set; it does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law, but it sits inside the certified discrete gravity layer those landmarks eventually constrain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.