e_330110
plain-language theorem explainer
For the concrete index sextuple (3,3,0,1,1,0) in (Fin 4)^6, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel cells that assemble the global m2Num = 8·explicitZ identity. The proof is a single decide on two closed integer expressions.
Claim. For indices $(a,b,c,d,i,j)=(3,3,0,1,1,0)$ with each coordinate in $\mathbb{F}_4$, the integer numerator $m_2^{\mathrm{num}}(3,3,0,1,1,0)$ obtained by folding coupling contributions equals $8\,Z(3,3,0,1,1,0)$, where $Z$ is the explicit closed-form kernel on the same indices.
background
This module is chunk 15 of a 256-cell kernel certification that the Regge midpoint $m_2$ numerator coincides with eight times an explicit integer table on every sextuple of 4D simplex indices.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term evaluated at those six Fin-4 indices. The comparison value $Z(a,b,c,d,i,j)$ is an explicit pattern-matched integer table (entries such as $4$, $-2$, and so on) on the same domain.
The local claim is only the single cell $(3,3,0,1,1,0)$. Sibling theorems cover the other cells; the assemble theorem glues them by exhaustive fin_cases.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers (the fold of contrib over couplingZList versus eight times the matched explicitZ entry), so the decidable equality of Int closes the goal with no further lemmas.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the universal quantifier by fin_cases into these cell theorems. That global identity is the algebraic core of the 4D Regge exact-midpoint $M_2$ TT certification in the Gravity analysis stack. Without each cell (including this one) the assemble step cannot finish. Landmark contact is indirect: it supports the discrete geometric side of RS gravity rather than a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.