e_210220
plain-language theorem explainer
For the six Fin-4 indices (2,1,0,2,2,0), the midpoint Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel cells that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a=2$, $b=1$, $c=0$, $d=2$, $i=2$, $j=0$ in $\mathrm{Fin}\,4$, the folded midpoint numerator equals eight times the explicit kernel integer: $\mathrm{m2Num}(2,1,0,2,2,0)=8\cdot\mathrm{explicitZ}(2,1,0,2,2,0)$.
background
In the 4D Regge midpoint analysis, the numerator m2Num is defined by folding a fixed coupling list: each term contributes an integer depending on six Fin-4 indices (two edge pairs and a midpoint pair). The companion explicitZ is a sparse pattern match that returns a small integer (typically $\pm 2$ or $4$) on the support of that kernel and zero elsewhere.
This module is chunk 9 of a 256-cell partition of the Fin-4^6 index space. The local goal, stated in the module header, is to certify m2Num = 8·explicitZ cell by cell so a later assembler can recombine them by exhaustive fin_cases.
The factor of eight is the combinatorial multiplicity that converts the folded coupling sum into the closed kernel table used downstream in the exact midpoint TT identity.
proof idea
One-line kernel decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are substituted: the left-hand side evaluates the fold that defines m2Num, the right-hand side multiplies the pattern value of explicitZ by eight. Lean’s decide closes the resulting integer equality with no lemmas beyond the two definitions.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in Fin-4 by cascading fin_cases and invoking one cell theorem per branch. That global equality is the algebraic certificate that the midpoint Regge numerator matches eight times the explicit 4D kernel, a step in the Gravity analysis chain toward the exact midpoint TT identity.
Within Recognition Science this sits in the discrete-geometry layer that underwrites continuum limits and effective gravitational couplings; it does not itself touch the T0–T8 forcing chain or the J-cost, but it hardens the combinatorial backbone those continuum claims rely on. Closing all 256 chunks removes scaffolding from the kernel certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.