e_111012
plain-language theorem explainer
For the six Fin-4 indices (1,1,1,0,1,2), the midpoint Regge numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it when assembling the full pointwise identity m2Num = 8·explicitZ over the 4D index cube. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=c=1$, $d=0$, $i=1$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the tabulated kernel integer $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each tuple. The comparison target $Z$ is an explicit piecewise table of small integers (entries such as $4$, $-2$, and so on on selected index patterns).
This module is chunk 5 of a 256-way kernel split: each declaration fixes one concrete six-tuple and asserts $m_2^{\mathrm{num}}=8Z$ at that point. The surrounding assemble theorem then recombines all chunks by exhaustive fin_cases on the six indices.
The local setting is pure finite discrete algebra over $\mathbb{Z}$; no continuum limit or curvature hypothesis is invoked inside the chunk.
proof idea
One-line closed proof: by decide. Lean evaluates both sides at the concrete indices $(1,1,1,0,1,2)$—the fold that defines $m_2^{\mathrm{num}}$ and the matching clause of the explicit $Z$ table—and checks integer equality. No lemmas beyond the two definitions are required.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by casing through all chunk certificates of this form. That global equality is the algebraic backbone of the exact midpoint $M_2$ TT identity in the 4D Regge analysis under Gravity.
Within Recognition Science gravity work, such kernel identities underwrite discrete curvature bookkeeping before continuum or phenomenological layers. The chunk does not itself touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder; it is infrastructure for the Regge side of the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.