e_311023
plain-language theorem explainer
For the six-index tuple (3,1,1,0,2,3) in 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 decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integer arithmetic.
Claim. For indices $a=3$, $b=1$, $c=1$, $d=0$, $i=2$, $j=3$ in $\mathrm{Fin}\,4$, the folded midpoint 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
This module is chunk 13 of a 256-way case split proving that the Regge midpoint numerator equals eight times an explicit integer kernel on all six-tuples in $(\mathrm{Fin},4)^6$. The setting is 4D discrete gravity analysis: couplings are summed into a numerator that should match a closed form used in exact midpoint identities.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a contribution function over a fixed coupling list, starting from zero. The explicit kernel $Z$ is a pattern-matched integer table on six $\mathrm{Fin},4$ indices (sample entries include $4$, $-2$, and so on for distinguished index patterns). Both live in the kernel-certificate module imported here.
The global claim is assembled downstream by exhausting all index combinations; each chunk theorem such as this one discharges one concrete six-tuple.
proof idea
One-line kernel decide. Lean reduces both sides of the equality on the fixed indices $(3,1,1,0,2,3)$ to concrete integers via the definitions of $m_2^{\mathrm{num}}$ (fold of contributions) and $Z$ (pattern match), then closes by decide. No lemmas beyond those definitions are invoked.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all six $\mathrm{Fin},4$ indices, proved by nested fin_cases that route each tuple to a chunk equality of this form. That global identity is the algebraic backbone of the exact midpoint M2/TT identity in the 4D Regge analysis stack.
Within Recognition Science gravity work, such kernel certificates pin discrete curvature/coupling numerics before continuum or phenomenological limits. This declaration is pure scaffolding closure for one of 256 cases, not a standalone physical law; its value is that the assemble step can quote a proved equality rather than a sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.