e_312030
plain-language theorem explainer
Pointwise identity: the midpoint Regge m2 numerator at multi-index (3,1,2,0,3,0) equals eight times the explicit Z kernel entry. Gravity analysts cite it as one of 256 Fin-4 kernel decides that assemble the global m2Num = 8·explicitZ theorem. The proof is a single kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,0,3,0)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathbb{F}_4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the given multi-index. The comparison target is an explicit piecewise integer table $Z$ on the same six indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
This module is chunk 13 of the 256-case kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ holds at every point of $(\mathbb{F}_4)^6$. The local setting is pure finite enumeration: no continuum limit or curvature hypothesis enters the equality itself.
proof idea
One-line kernel proof: decide evaluates both sides as concrete Int values for the fixed six indices and checks equality. No lemmas beyond the definitions of the folded numerator and the explicit table are required; the tactic discharges the closed arithmetic goal.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathbb{F}_4$, $m_2^{\mathrm{num}}=8\cdot Z$ by exhaustive fin_cases over all six indices, invoking each chunk identity such as this one. That global identity is the algebraic core of the Regge exact midpoint M2/TT certification in 4D gravity analysis inside the monolith. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is infrastructure for the discrete curvature/mass-side bookkeeping those layers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.