e_312320
plain-language theorem explainer
Single kernel identity: the folded coupling numerator at multi-index (3,1,2,3,2,0) equals eight times the closed-form table entry. Gravity analysts cite it only as one of the 256 concrete cases that assemble the full six-index midpoint identity. The proof is a pure `decide` on fixed Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,3,2,0)$ in $(\mathrm{Fin}\,4)^6$, the summed coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(3,1,2,3,2,0)=8\,Z_{\mathrm{expl}}(3,1,2,3,2,0)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each multi-index. The comparison target $Z_{\mathrm{expl}}$ is an explicit piecewise table of small integers (entries such as $4$, $-2$, and so on) on the same index domain.
The local module is chunk 13 of a 256-way case split whose sole job is to prove $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ pointwise. Each chunk theorem fixes one concrete six-tuple and discharges the integer equality by computation. Upstream, both kernels live in the KernelCert module; downstream they are reassembled by exhaustive fin_cases.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are substituted, so the kernel decision procedure closes the equality with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by nested fin_cases and consumes the 256 chunk equalities (this one among them). That global identity is the algebraic core of the Regge exact-midpoint $M_2$ TT certificate in the Gravity analysis stack. It does not itself touch the forcing chain (T0–T8), RCL, or the phi-ladder mass formula; it is pure discrete kernel bookkeeping needed before continuum or phenomenological gravity claims can be attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.