e_010302
plain-language theorem explainer
At multi-index (0,1,0,3,0,2), the folded coupling numerator equals eight times the explicit integer table entry. Gravity analysts cite it as one of 256 kernel point checks for the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,3,0,2)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-way case split proving that the 4D Regge midpoint numerator equals eight times a closed-form integer table. The ambient setting is exact algebraic certification of an M2TT identity used in discrete gravity analysis.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling triple at the six $\mathrm{Fin},4$ indices. The table $Z$ is an explicit pattern-matched integer function on the same six indices (typical values $\pm 2,,4$ on the listed patterns).
The parent goal is the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$, assembled by exhausting all $4^6$ index tuples via fin_cases. Each chunk theorem discharges one concrete tuple.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete integers (the fold of contributions versus eight times the matched table entry), so the equality is a decidable Int fact with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the full six-index identity by casing on every $\mathrm{Fin},4$ coordinate and invoking the matching chunk. Without these pointwise facts the assembly cannot close.
In the gravity stack this certifies that the midpoint M2TT numerator is exactly eight times the explicit $Z$ table, an algebraic identity needed for exact (non-approximate) Regge analysis in four dimensions. It is bookkeeping inside the discrete-gravity certification path, not a new physical law; it locks the numerator side of the midpoint identity so later curvature or continuum-limit arguments can quote a proved closed form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.