e_003203
plain-language theorem explainer
For the single index sextuple (0,0,3,2,0,3), the folded Regge midpoint mass-squared numerator equals eight times the explicit Z-coupling table entry. Gravity analysts cite it as one atomic kernel cell in the 4^6 case split. The proof is a pure `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,0,3,2,0,3)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge midpoint analysis of the Recognition gravity stack. The local goal, stated in the module header, is to certify the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on one 256-cell chunk of the six-index kernel over $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums a contribution functional over that list at the six indices. The comparison object $Z$ is an explicit integer table on $(\mathrm{Fin},4)^6$, given by pattern-matching clauses (e.g. value $4$ on diagonal-type slots, $-2$ on selected off-diagonal slots, and $0$ elsewhere).
The present declaration fixes one concrete sextuple inside chunk 0 and asserts numerical equality at that point only.
proof idea
One-line computational discharge: both sides reduce to closed integer expressions once the six indices are literals, so decide evaluates the fold that defines the numerator against the matching clause (or default) of the explicit $Z$ table and checks equality in $\mathbb{Z}$. No lemmas are invoked beyond the two defining defs.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states the identity for every sextuple in $(\mathrm{Fin},4)^6$ and closes the goal by exhaustive fin_cases on the six indices. Each chunk cell such as this one supplies a named, machine-checked witness for one branch of that case tree, so the global midpoint $M_2$ numerator identity is only as strong as the conjunction of these decides.
In the broader RS gravity line this is bookkeeping infrastructure, not a new physical law: it underwrites exact algebraic control of the Regge midpoint mass-squared kernel in 4D before continuum or phenomenological limits are taken. It does not itself touch the forcing chain (T0–T8), $\varphi$, or the $\alpha$ band; it is a finite combinatorial certificate inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.