e_022303
plain-language theorem explainer
For the six Fin-4 indices (0,2,2,3,0,3), the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over the 4D Regge midpoint stencil. The proof is a single kernel decide on the concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}2$, $d{=}3$, $i{=}0$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint analysis: it certifies the pointwise identity numerator = 8 · closed form on a block of the $4^6$ index tuples (module doc: "m2Num = 8·explicitZ, chunk 2 (256 kernel decides)").
The numerator m2Num is defined by folding a fixed coupling list: start at 0 and add each local contribution contrib t a b c d i j. The closed form explicitZ is an integer-valued pattern match on the six Fin-4 indices (sample clauses return 4, −2, etc.). Both live in the KernelCert module imported here.
The local goal is purely algebraic bookkeeping: evaluate both sides on one concrete sextuple and record equality so a later assembler can cover the full product of Fin-4 factors by case split.
proof idea
One-line decide proof. Lean reduces m2Num 0 2 2 3 0 3 by unfolding the fold over couplingZList and summing the integer contributions, reduces explicitZ 0 2 2 3 0 3 by the pattern-match table, multiplies by 8, and checks the two Int values are definitionally equal. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by nested fin_cases and consumes each chunk equality such as this one. That global identity is the numerical backbone of the Regge exact-midpoint M2/TT analysis in the Gravity domain: it replaces a folded coupling sum by an explicit sparse kernel, enabling exact (not approximate) midpoint identities in the discrete curvature calculus.
Within Recognition Science this sits in the gravity/Regge layer rather than the T0–T8 forcing chain; it is infrastructure that keeps the discrete geometric side exact so continuum limits and mass/ladder comparisons remain free of numerical residue. No open scaffold remains on this sextuple: the decide closes it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.