e_311231
plain-language theorem explainer
For the six-index tuple (3,1,1,2,3,1) on Fin 4, the midpoint Regge numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite this as one of the 256 kernel point-checks that assemble the global identity. The proof is a single kernel decide on integer arithmetic.
Claim. For indices $a=3$, $b=1$, $c=1$, $d=2$, $i=3$, $j=1$ in $\mathrm{Fin}\,4$, the folded midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer depending on six Fin-4 indices, and the fold starts from zero. The companion map explicitZ is a sparse closed-form table on those same six indices (nonzero only on a short list of patterns such as $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local module is chunk 13 of a 256-way case split: the claim is that $m_2^{\mathrm{num}}=8\cdot Z$ holds pointwise on every index sextuple. This file discharges one concrete sextuple by kernel decision; sibling chunks cover the remaining points.
Upstream, both $m_2^{\mathrm{num}}$ and explicitZ live in the kernel certificate module that packages the coupling list and the explicit table used throughout the midpoint identity.
proof idea
One-line proof by decide. Lean evaluates both sides as concrete integers: the left-hand side runs the fold of coupling contributions at indices $(3,1,1,2,3,1)$, the right-hand side multiplies the table value of explicitZ at those indices by eight, and the kernel checks equality.
why it matters
Feeds the assembler theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all Fin-4 indices, which proceeds by exhaustive fin_cases and invokes each point lemma such as this one. That global identity is the algebraic core of the exact midpoint $M_2$ TT identity in 4D Regge calculus inside the Gravity analysis stack.
Within Recognition Science this sits in the discrete-gravity layer that must match continuum curvature bookkeeping; it does not itself invoke the forcing chain (T5–T8) or the J-cost, but it is infrastructure for the Regge side of the gravity bridge. Closing all 256 chunks removes scaffolding from the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.