e_030303
plain-language theorem explainer
For the six-index tuple (0,3,0,3,0,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one cell of the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=0$, $b=3$, $c=0$, $d=3$, $i=0$, $j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,3,0,3,0,3)=8\,Z(0,3,0,3,0,3)$.
background
This module is chunk 3 of a 256-cell kernel certification that the Regge midpoint numerator m2Num agrees with eight times a closed-form table explicitZ on all six-tuples in $(\mathrm{Fin},4)^6$.
m2Num a b c d i j is defined by folding a fixed coupling list, accumulating integer contributions at those indices. explicitZ is a pattern-matched integer table on the same six indices (sample values include $4$, $-2$, and other small integers on distinguished patterns).
The local goal is purely algebraic bookkeeping: each chunk discharges a block of concrete equalities so the assembler can rebuild the universal identity without re-running the full fold.
proof idea
One-line decide proof. Both sides reduce to concrete Int values for the fixed indices $(0,3,0,3,0,3)$: the left via the fold definition of the numerator, the right via the pattern match on the explicit kernel (scaled by 8). Lean’s kernel decision procedure checks integer equality; no lemmas are invoked.
why it matters
Feeds m2Num_eq_eight_explicitZ in the assemble module, which states $\forall a,b,c,d,i,j,; N=8Z$ and proves it by exhaustive fin_cases on all six Fin 4 arguments, routing each cell to a chunk theorem such as this one.
In the Recognition gravity stack this identity is infrastructure for the exact 4D Regge midpoint M2/TT analysis: it replaces a folded coupling sum by a sparse closed-form kernel, enabling later curvature and continuum-limit arguments. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is a certified arithmetic step inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.