e_033120
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at multi-index (0,3,3,1,2,0) equals eight times the explicit integer kernel at those same Fin-4 slots. Gravity analysts cite it when assembling the full 4D Regge midpoint M2–TT numerator identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,1,2,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(0,3,3,1,2,0)=8\,Z_{\mathrm{expl}}(0,3,3,1,2,0)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator side $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it accumulates every local contribution contrib over couplingZList, starting from 0. The comparison side $Z_{\mathrm{expl}}$ is an explicit pattern-matched table of small integers (entries such as $4$, $-2$, and so on) on the same six-index domain.
The module is chunk 3 of a 256-way kernel split whose sole job is to discharge $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ at concrete multi-indices by decision procedure. Upstream, both m2Num and explicitZ live in the kernel-certificate module; this chunk only evaluates them at fixed slots.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are literals $(0,3,3,1,2,0)$, so the kernel equality is a closed integer fact with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhaustive fin_cases and invokes each chunk pointwise. That global equality is the algebraic core of the 4D Regge midpoint M2–TT numerator certificate in the Gravity analysis stack. It is bookkeeping, not a new physical law: once every chunk holds, the folded coupling is identically eight times the explicit kernel, clearing the numerator side of the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.