e_321223
plain-language theorem explainer
For the six-index tuple (3,2,1,2,2,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one cell in the 4D Regge midpoint M2TT identity table. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3,b{=}2,c{=}1,d{=}2,i{=}2,j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(3,2,1,2,2,3)=8\,Z(3,2,1,2,2,3)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $N(a,b,c,d,i,j)$ is obtained by folding a fixed coupling list and summing each term's contribution at those indices. The closed form $Z$ is an explicit pattern-matched integer table (typical entries $\pm 2,,4$, and so on).
The module is chunk 14 of a 256-cell decide grid that checks $N=8Z$ pointwise. The ambient claim is the exact midpoint M2TT identity in four dimensions: after all cells assemble, the folded numerator is identically eight times the explicit kernel on every index tuple.
proof idea
One-line decide on fully concrete Fin-4 arguments. Both sides reduce to closed integers (the fold for $N$ and the pattern match for $Z$), so the kernel discharges the equality without lemmas or case splits inside this declaration.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases over Fin 4. Each chunk theorem such as this one is a leaf of that case tree (or an equivalent decide grid). In the gravity stack this identity is the algebraic certificate that the midpoint Regge M2TT numerator matches the explicit kernel normalization, a prerequisite for the continuum/Regge comparison steps downstream. It is bookkeeping, not a new physical law, but the full forall is only as strong as every cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.