e_003232
plain-language theorem explainer
For the six-index tuple (0,0,3,2,3,2) on Fin 4, the folded numerator m2Num equals eight times the tabulated explicit kernel value. Gravity analysts cite it as one cell of the 4D Regge midpoint M2TT certificate. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,0,3,2,3,2)$ in $(\mathbb{F}_4)^6$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is one 256-cell chunk of the 4D Regge exact-midpoint M2TT identity certificate: the claim that the folded numerator equals eight times a closed-form kernel on every multi-index in $(\mathbb{F}_4)^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list, accumulating integer contributions at the six Fin-4 slots. The explicit kernel $Z$ is a pattern-matched integer table on those same slots (typical values $\pm 2,4$, etc.).
Local setting (module doc): prove $m_2^{\mathrm{num}}=8\cdot Z$ cell-by-cell via kernel decides, then reassemble.
proof idea
One-line computational proof: decide evaluates both sides at the concrete indices $(0,0,3,2,3,2)$ and checks integer equality. No lemmas are invoked beyond the definitions of the fold numerator and the explicit table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 indices by exhaustive fin_cases and discharges each cell with a chunk theorem of this form. That global equality is the algebraic core of the Regge exact-midpoint M2TT identity in 4D gravity analysis inside the monolith. It is bookkeeping infrastructure, not a forcing-chain landmark (T5–T8), but it certifies the discrete curvature/coupling numerator used downstream in the gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.