e_021310
plain-language theorem explainer
For the six-index slot (0,2,1,3,1,0) on Fin 4, the midpoint Regge numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite these micro-identities when assembling the global m2Num = 8·explicitZ certificate. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}1$, $d{=}3$, $i{=}1$, $j{=}0$ in $\mathrm{Fin}\,4$, the folded midpoint numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the tabulated kernel entry $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator side m2Num folds a fixed coupling list, summing a local contribution at each tuple. The comparison side explicitZ is a sparse case table of small integers (entries such as $4$, $-2$, and defaults).
The module is one chunk of a 256-way case split that discharges the pointwise identity $\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$. Chunk 2 holds a block of these concrete equalities; each is an independent kernel decision on fixed indices.
Upstream, explicitZ and m2Num are pure definitions in the kernel certificate module, so the only content to check is arithmetic equality of two closed integer expressions at the given slot.
proof idea
One-line decide proof. Both sides reduce to concrete Int values once the six indices are substituted into the fold definition of the numerator and the case table of the explicit kernel; the kernel then verifies the equality $n=8z$ by computation. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for all six indices by exhaustive fin_cases and invokes each chunk equality such as this one. That global certificate is part of the Regge exact-midpoint $M_2$ TT-identity work in the gravity analysis stack: it replaces a symbolic coupling sum by an eightfold multiple of a sparse explicit table, simplifying later curvature and mass-ladder checks.
Within Recognition Science this sits in the gravity sector rather than the T0–T8 forcing chain; it is infrastructure that keeps the discrete geometric side exact before continuum or observational claims are attached. Closing every chunk removes scaffolding from the midpoint identity path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.