e_031302
plain-language theorem explainer
For the six-index tuple (0,3,1,3,0,2) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite these pointwise identities when assembling the global Regge midpoint M2–TT relation. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}3$, $c{=}1$, $d{=}3$, $i{=}0$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the tabulated explicit kernel entry: $N(0,3,1,3,0,2)=8\,Z(0,3,1,3,0,2)$.
background
This module sits in the Gravity analysis stack that certifies an exact midpoint identity for the Regge M2–TT sector in 4D. The local goal, stated in the module header, is to prove the pointwise relation numerator = 8 · explicit kernel on a 256-case chunk of the Fin-4 index space.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add a contribution for each coupling term at those six indices. The explicit kernel $Z$ is a closed integer table on $(\mathrm{Fin},4)^6$, with nonzero values such as $\pm 2$ and $4$ on selected patterns and (implicitly) 0 elsewhere.
Chunk 3 is one of several sibling modules that discharge individual index sextuples so a later assembler can recombine them by exhaustive fin_cases.
proof idea
One-line proof by decide. Both sides are closed integer expressions once the six Fin-4 indices are fixed: the left side evaluates the fold of contributions over the coupling list; the right side is eight times the matching clause (or default) of the explicit kernel table. Lean’s kernel decision procedure checks the resulting integer equality.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and proves it by six nested fin_cases over Fin 4, invoking one chunk lemma per concrete tuple. Without these pointwise certificates the global Regge midpoint M2–TT identity in 4D cannot be discharged in Lean.
In the broader Recognition gravity stack this is bookkeeping infrastructure rather than a new physical law: it locks the discrete curvature/coupling algebra so continuum or continuum-limit claims built on the exact midpoint identity rest on a fully expanded integer kernel. It does not itself invoke the forcing chain (T5–T8), RCL, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.