e_322203
plain-language theorem explainer
For the six-index tuple (3,2,2,2,0,3) on Fin 4, the folded Regge midpoint numerator m2Num equals eight times the explicit kernel value explicitZ at those indices. Gravity analysts assembling the full 4D midpoint identity cite this as one of the 256 kernel point checks. The proof is a single `decide` on concrete integer arithmetic.
Claim. For indices $a{=}3$, $b{=}2$, $c{=}2$, $d{=}2$, $i{=}0$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
In the Regge exact-midpoint analysis, m2Num is the integer obtained by folding a fixed coupling list: start at 0 and add each term's contribution at a six-index slot $(a,b,c,d,i,j)$ with each index in $\mathrm{Fin},4$. The companion explicitZ is a sparse lookup table of small integers (entries such as $4$, $-2$, and so on) on the same six-index domain.
This module is chunk 14 of a 256-way partition of that domain. The local claim is the pointwise identity $m_2^{\mathrm{num}} = 8\cdot Z$ at one concrete multi-index, so that a later exhaustive assembly can glue the chunks into a universal statement.
proof idea
One-line computational discharge: decide evaluates both sides as concrete Int expressions (the fold for the numerator and the table lookup for $Z$) and checks equality. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$, proved by six nested fin_cases. Each leaf is a chunk identity of this form; this declaration covers the leaf $(3,2,2,2,0,3)$.
In the gravity stack that identity certifies that the midpoint $M_2$ numerator is exactly eight times the explicit kernel, a numerical hinge in the 4D Regge midpoint TT analysis. It is pure kernel bookkeeping, not a forcing-chain step (T0–T8), but it is required scaffolding for the exact midpoint identities used downstream in the gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.