e_302011
plain-language theorem explainer
For the six-index tuple (3,0,2,0,1,1) on Fin 4, the midpoint Regge numerator m2Num equals eight times the closed-form kernel value 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 integers.
Claim. For indices $a=3$, $b=0$, $c=2$, $d=0$, $i=1$, $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 kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 12 of a 256-case kernel certification that the four-dimensional Regge midpoint numerator equals eight times a closed-form integer table. The ambient setting is discrete gravity analysis: edge couplings on a 4-simplex midpoint scheme, with all free indices ranging over $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each tuple $(a,b,c,d,i,j)$. The comparison object $\mathrm{explicitZ}$ is a hand-written integer table on the same six indices (typical values $\pm 2,,4$ on the listed patterns, and zero or other constants off those patterns).
The global claim is that these two agree up to the universal factor 8 for every index combination. Each chunk theorem discharges one concrete combination so the assembler can finish by exhaustive fin_cases.
proof idea
One-line kernel decide. Both sides evaluate to concrete integers once the six Fin-4 arguments are fixed: the left side by folding the coupling list, the right side by looking up the explicit table and multiplying by 8. Lean’s decide closes the equality of those integers; no algebraic lemmas are invoked.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states the identity for all $a,b,c,d,i,j:\mathrm{Fin},4$ by casing on each index and invoking the 256 chunk facts. That global equality is the certified algebraic core of the Regge exact-midpoint $M_2$ TT identity in 4D: it replaces a folded sum by a sparse closed-form kernel, which is what later gravity lemmas quote when they simplify curvature or mass-side expressions.
Within Recognition Science gravity work this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8). It does not touch $\phi$, the eight-tick octave, or the $\alpha$ band; it only guarantees that the discrete midpoint numerator used downstream is exactly eight times the tabulated kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.