e_310330
plain-language theorem explainer
For the Fin-4 multi-index (3,1,0,3,3,0), the folded mass-squared coupling numerator equals eight times the tabulated explicit kernel entry. Gravity analysts certifying the 4D Regge midpoint M2TT identity cite this as one concrete kernel case among the chunked decides. The proof is a single kernel `decide` on integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,3,3,0)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel table value at that multi-index.
background
In the 4D Regge exact-midpoint analysis, the mass-squared numerator is defined by folding a contribution map over a fixed coupling list: each six-tuple of $\mathrm{Fin},4$ indices accumulates an integer. A companion table records closed-form integer kernel values for the same multi-indices (e.g. pattern-matched entries such as $4$, $-2$, and so on).
This module is chunk 13 of the case-split that asserts the numerator equals eight times the explicit table on every multi-index. The local setting is pure finite integer arithmetic: no continuum limit, no floating-point residual. Upstream, the two definitions supply the left- and right-hand sides that each concrete case equates.
proof idea
One-line wrapper by decide. Both sides are closed integer terms: the left folds contributions over the coupling list at the fixed indices $(3,1,0,3,3,0)$; the right is the pattern-match value of the explicit kernel table at those same indices. The kernel reduces both to numerals and checks equality.
why it matters
Parent theorem m2Num_eq_eight_explicitZ universalizes the identity over all $\mathrm{Fin},4$ sextuples by nested fin_cases, dispatching each concrete goal to a chunk lemma of this form. Without the chunk decides, the assemble proof cannot close.
In the broader Recognition gravity stack this is bookkeeping for the exact midpoint M2TT identity in 4D Regge calculus: it certifies that the numerator coupling factors exactly as $8$ times a sparse explicit kernel, a prerequisite for later continuum or continuum-limit comparisons. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is infrastructure inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.