e_001301
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (0,0,1,3,0,1) equals eight times the closed-form integer table at that same point. One of 256 kernel cells assembled into the global statement that the numerator is identically 8·explicitZ on (Fin 4)^6. Proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,0,1,3,0,1)\in(\mathbb{F}_4)^6$, the summed coupling numerator equals eight times the explicit integer table entry: $m_2^{\mathrm{num}}(0,0,1,3,0,1)=8\,Z_{\mathrm{expl}}(0,0,1,3,0,1)$.
background
This module is chunk 0 of a 256-cell kernel certifying that the Regge midpoint $M_2$ numerator equals eight times a closed-form integer table on all of $(\mathrm{Fin},4)^6$. The setting is the exact midpoint $M_2$ TT identity in 4D discrete gravity analysis.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each local contribution at the six indices. The table $Z_{\mathrm{expl}}$ is an explicit case-split $\mathrm{Fin},4^6\to\mathbb{Z}$ (sparse nonzero pattern, e.g. values in ${4,-2,\ldots}$ on selected index patterns).
The global claim is assembled downstream by exhausting all six $\mathrm{Fin},4$ coordinates; each cell such as this one discharges one concrete tuple.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six indices are fixed literals in $\mathrm{Fin},4$, so the kernel decision procedure checks equality with no further lemmas. No algebraic rewriting is required beyond evaluation of m2Num (the fold) and explicitZ (the case table).
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 $\mathrm{Fin},4$, dispatching each of the 256 cells to a chunk identity of this form.
In the gravity analysis stack this identity is bookkeeping for the exact midpoint $M_2$ TT relation in 4D Regge-type discrete curvature: once the numerator is identified with the explicit table, later steps can treat $Z_{\mathrm{expl}}$ as the closed form rather than the fold. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure finite combinatorial certification inside the gravity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.