e_213302
plain-language theorem explainer
For the six-index tuple (2,1,3,3,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one cell of the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}1$, $c{=}3$, $d{=}3$, $i{=}0$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling 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
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each term's contribution at the given indices. The companion map explicitZ is a sparse lookup that returns small integers (typically $\pm 2$ or $4$) on selected index patterns and is the closed form the fold is meant to match.
This module is chunk 9 of a 256-cell decide grid that checks $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The factor of eight is the global normalization relating the folded sum to the explicit kernel. The ambient goal is an exact algebraic identity for the midpoint M2 tensor structure in discrete gravity, not a continuum limit statement.
proof idea
One-line decide on fully concrete Fin-4 arguments. Both sides reduce to closed integers: the left via the fold definition of m2Num over couplingZList, the right via the pattern match in explicitZ scaled by 8. No lemmas are invoked beyond kernel evaluation of the two defs.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 indices by exhaustive fin_cases. Each chunk theorem such as this one discharges one cell so the universal statement can be built without a single monolithic decide. In the gravity stack this underwrites the exact midpoint M2 TT identity used in the discrete curvature bookkeeping; it is pure integer algebra on the coupling kernel, not a dynamical field equation. No Recognition forcing-chain landmark (T5–T8, RCL, phi) is directly at stake here; the result is infrastructure for the Regge analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.