e_102332
plain-language theorem explainer
Single-index check that the Regge midpoint mass-squared numerator equals eight times the explicit Z-kernel at Fin-4 indices (1,0,2,3,3,2). Gravity analysts assembling the 4D midpoint M2–TT identity cite it as one cell of the 4^6 case table. Proof is a kernel `decide` on the unfolded integer equality.
Claim. For indices $(a,b,c,d,i,j)=(1,0,2,3,3,2)$ 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, the mass-squared numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at six Fin-4 indices, and the fold starts from 0. The companion table $Z$ (explicitZ) is a closed-form Int-valued kernel on the same six indices, with sparse nonzero entries such as $4$ on matched pairs and $-2$ on crossed pairs.
This module is chunk 4 of the certified equality $m_2^{\mathrm{num}}=8\cdot Z$. The local setting is pure finite enumeration: every 6-tuple in $(\mathrm{Fin},4)^6$ is a separate decide goal. Upstream, both $m_2^{\mathrm{num}}$ and $Z$ live in the KernelCert module; the present theorem only evaluates them at one concrete point.
proof idea
One-line kernel proof: decide. Lean unfolds the fold definition of $m_2^{\mathrm{num}}$ at $(1,0,2,3,3,2)$, evaluates the matching clause of $Z$, multiplies by 8, and checks integer equality by computation. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembled universal statement m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j., m_2^{\mathrm{num}}=8\cdot Z$ by exhausting Fin-4 cases. That identity is the algebraic core of the Regge exact midpoint M2–TT certificate in four dimensions: once numerator and explicit kernel agree up to the factor 8, the continuum TT matching can quote a single closed form instead of a fold.
Within Recognition gravity work this is bookkeeping, not a new physical law. It does not touch the forcing chain (T0–T8), the J-cost, or the phi ladder; it only clears one cell so the 4D midpoint mass kernel is fully certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.