e_313130
plain-language theorem explainer
One of 256 concrete kernel identities: the folded midpoint numerator at multi-index (3,1,3,1,3,0) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the universal m2Num = 8·explicitZ identity over (Fin 4)^6. The proof is a single kernel decide on fixed integers.
Claim. For the multi-index $(3,1,3,1,3,0)\in(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit $Z$-table value: $m_2^{\mathrm{num}}(3,1,3,1,3,0)=8\,Z_{\mathrm{expl}}(3,1,3,1,3,0)$.
background
This module is chunk 13 of a 256-way split that certifies, index by index, the algebraic identity between two integer-valued kernels on six Fin 4 arguments in the 4D Regge midpoint analysis.
The folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by left-folding a fixed coupling list and summing a local contribution at each term. The comparison object $Z_{\mathrm{expl}}$ is an explicit case table Fin 4^6 → ℤ (sample entries include $4$ on diagonal pairs such as $(0,0,1,1,2,2)$ and $-2$ on mixed pairs such as $(0,0,1,2,1,2)$).
The local claim is the single tuple $(3,1,3,1,3,0)$ inside that table-versus-fold comparison.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple of Fin 4 values and checks integer equality. No lemmas are invoked; the kernel reduces the fold defining the numerator and the matching clause of the explicit table to numerals and compares them.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and discharges the universal quantifier by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is one cell of that 256-cell kernel certificate.
In the broader gravity stack this identity is bookkeeping for the exact midpoint Regge $M_2$ TT sector in 4D: it guarantees the folded coupling numerator is a pure multiple of the closed-form $Z$ table, so later curvature and mass-ladder arguments can quote the table instead of re-expanding the fold. It does not itself touch T5–T8 or the RCL; it is infrastructure under the discrete gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.