e_310332
plain-language theorem explainer
For the six-index tuple (3,1,0,3,3,2) on Fin 4, the folded numerator coupling m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts assembling the exact midpoint Regge M2-TT identity cite this as one of the 256 kernel cases. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}1$, $c{=}0$, $d{=}3$, $i{=}3$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded numerator coupling equals eight times the explicit integer kernel value at those indices: $N(3,1,0,3,3,2)=8\,Z(3,1,0,3,3,2)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices appear. The numerator coupling $N(a,b,c,d,i,j)$ is obtained by folding a fixed coupling list and summing elementary contributions at those indices. The explicit kernel $Z$ is a closed pattern-match table returning small integers (typically $\pm 2,\pm 4$, or $0$) on each six-tuple.
The local module is chunk 13 of a 256-case kernel certification that $N=8Z$ pointwise. The identity is the algebraic backbone of the midpoint M2-TT comparison in the gravity analysis stack; each chunk discharges a block of concrete index combinations so the global statement can be assembled by exhaustive case split on $\mathrm{Fin},4$.
proof idea
One-line kernel proof: decide. Both sides evaluate to concrete integers (the fold for $N$ and the match for $Z$), so the equality is a closed arithmetic fact with no further lemmas.
why it matters
This case is consumed by the assembler theorem asserting $\forall a,b,c,d,i,j,, N=8Z$ on $\mathrm{Fin},4^6$, proved by nested fin_cases. Without the chunk equalities the global midpoint identity does not close. In the Recognition gravity stack the factor-of-eight relation between the folded numerator and the explicit kernel is the exact algebraic certificate used downstream of the Regge midpoint reduction; it is infrastructure for the discrete curvature side rather than a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.