e_001030
plain-language theorem explainer
At multi-index $(0,0,1,0,3,0)$, the folded Regge coupling numerator equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full $m_2=8Z$ identity over all $\mathrm{Fin}\,4$ sextuples. The proof is a single kernel `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,0,1,0,3,0)$ in $(\mathrm{Fin}\,4)^6$, the coupling numerator obtained by folding the contribution list equals $8$ times the explicit closed-form integer assigned to that multi-index.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on sextuples of $\mathrm{Fin},4$ indices are compared. The numerator $m_2$ is defined by folding a fixed coupling list: each term contributes an integer depending on the six indices, and the fold starts from zero. The companion map $Z$ is an explicit case table on the same index type, returning small integers such as $4$, $-2$, and so on for the patterns that appear.
This module is chunk 0 of a 256-way kernel split: each declaration checks one concrete sextuple of the identity $m_2=8Z$. The local setting is pure finite enumeration over $\mathrm{Fin},4$, with no analytic remainder.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,0,1,0,3,0)$ and confirms integer equality. No lemmas are invoked beyond the elaborator’s evaluation of the fold defining the numerator and the match defining the explicit table.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ proves the identity for every sextuple by nested fin_cases, discharging each leaf with a chunk theorem of this form. Without the per-index kernel facts, the universal statement cannot close. In the gravity stack this underwrites the exact midpoint $M_2$–$TT$ identity in 4D Regge calculus, a discrete curvature bookkeeping step inside the broader Recognition gravity analysis. It does not itself touch the forcing chain (T0–T8) or the J-cost; it is infrastructure for the discrete geometric side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.