e_020003
plain-language theorem explainer
Finite-index certificate: the coupling numerator at multi-index (0,2,0,0,0,3) equals eight times the explicit integer kernel at those same indices. Gravity analysts assembling the 4D Regge midpoint M2 TT identity cite it as one cell of the exhaustive Fin-4 table. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,0,0,3)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued tensors on $(\mathrm{Fin},4)^6$ are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer depending on the six indices, and the total is their sum. The companion $Z$ is an explicit sparse kernel: only a handful of index patterns are nonzero (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$), with all other sextuples defaulting by the match.
The local module is chunk 2 of the identity $m_2^{\mathrm{num}}=8\cdot Z$. Because both sides are pure integer functions of six finite indices, the universal claim reduces to a finite table of equalities, of which this declaration is one cell.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple $(0,2,0,0,0,3)$ and checks integer equality. No algebraic lemmas are invoked; the kernel reduces m2Num via the fold definition and explicitZ via its match, then compares the resulting Int literals.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 sextuple into the single identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$, by exhaustive fin_cases. This chunk supplies one of those cells (module doc: chunk 2, 256 kernel decides). In the broader gravity stack it is bookkeeping for the exact midpoint M2 TT identity in 4D Regge calculus, not a forcing-chain (T0–T8) step. It closes no open physics question by itself; it only discharges one concrete index combination so the universal assembly can succeed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.