e_100331
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (1,0,0,3,3,1) equals eight times the explicit integer table entry. Gravity analysts cite it as one of 256 kernel cells assembling the global m2Num = 8·explicitZ statement. Proof is a single decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(1,0,0,3,3,1)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the closed-form table: $m_2^{\mathrm{num}}(1,0,0,3,3,1)=8\,Z_{\mathrm{expl}}(1,0,0,3,3,1)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on $(\mathrm{Fin},4)^6$ are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the six indices. The companion $Z_{\mathrm{expl}}$ is an explicit pattern-matched table of small integers (entries such as $4$, $-2$, and so on).
This module is chunk 4 of a 256-cell kernel certification whose module slogan is "$m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$." Each cell fixes one concrete sextuple and checks the scalar identity. The ambient goal is an exact midpoint mass-squared / TT identity used in the gravity sector of the Recognition calculus.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel decision procedure discharges equality with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by six nested fin_cases over Fin 4, invoking one chunk cell per branch. Without the full 256-cell cover the global identity does not close.
In the gravity analysis this identity certifies that the folded coupling numerator is exactly eight times the closed-form table, a bookkeeping step toward the exact midpoint M2/TT relation in 4D Regge calculus. It is pure integer kernel arithmetic, not a dynamical field equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.