e_020332
plain-language theorem explainer
For the six-index slot (0,2,0,3,3,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these pointwise identities when assembling the global Regge midpoint M2TT relation in 4D. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}0$, $d{=}3$, $i{=}3$, $j{=}2$ in $\mathrm{Fin}\,4$, the summed coupling numerator equals eight times the explicit integer kernel: $N(0,2,0,3,3,2)=8\,Z(0,2,0,3,3,2)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $N=m2Num$ is defined by folding a fixed coupling list and summing local contributions at $(a,b,c,d,i,j)$. The comparison target $Z=explicitZ$ is a sparse closed-form table of small integers (entries such as $4$, $-2$, and defaults).
The module is chunk 2 of a 256-way case split: each theorem pins one concrete six-tuple so that the global identity $N=8Z$ can be reassembled by exhaustive fin_cases. The setting is pure integer arithmetic on a finite index set; no continuum limit or metric signature is invoked at this layer.
proof idea
One-line decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are literals: the fold defining the numerator evaluates fully, and the pattern match for the explicit kernel returns a fixed integer. Lean’s kernel decision procedure checks equality of the two computed integers.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by nested fin_cases over Fin 4. That global identity is the algebraic backbone of the Regge-exact midpoint M2TT certificate in 4D gravity analysis inside the monolith. Without the pointwise chunk lemmas, the assembler has nothing to discharge. The result is bookkeeping, not a new physical law: it certifies that the folded coupling sum matches the hand-written kernel at this slot, supporting later curvature or deficit identities built on the certified numerator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.