e_013020
plain-language theorem explainer
For the six-index tuple (0,1,3,0,2,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic cell in the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}3$, $d{=}0$, $i{=}2$, $j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,1,3,0,2,0)=8\,Z(0,1,3,0,2,0)$.
background
This module is chunk 1 of a 256-cell kernel certification that the Regge midpoint numerator m2Num equals eight times a closed-form integer table explicitZ on all six-tuples in $(\mathrm{Fin},4)^6$.
m2Num a b c d i j is defined by folding a fixed coupling list: start at 0 and add each local contribution contrib t a b c d i j. explicitZ is the sparse integer table that records the expected closed form (examples: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and so on).
The local setting is pure finite enumeration: every cell is an equality of two concrete integers, discharged by the kernel rather than by algebraic rewriting of the fold.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed indices $(0,1,3,0,2,0)$: the left via the fold definition of the numerator, the right via the pattern table for the explicit kernel (scaled by 8). No lemmas are invoked beyond decidable equality on integers.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for every six-tuple by fin_cases on each index and dispatches to these chunk cells. That global equality is the certified numerator half of the 4D Regge exact-midpoint M2/TT identity used in the gravity analysis stack.
Within Recognition Science this is bookkeeping infrastructure for discrete curvature/edge couplings on the 4-index simplex data, not a forcing-chain landmark (T5–T8). It closes one of the 256 decide cells so the assembler can finish without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.