e_212301
plain-language theorem explainer
For the six-index tuple (2,1,2,3,0,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}1$, $c{=}2$, $d{=}3$, $i{=}0$, $j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $\mathrm{m2Num}(2,1,2,3,0,1)=8\cdot\mathrm{explicitZ}(2,1,2,3,0,1)$.
background
This module is chunk 9 of a 256-cell kernel certification that the 4D Regge midpoint numerator m2Num coincides with eight times a closed-form table explicitZ. Both live in the KernelCert module: m2Num folds couplingZList, accumulating integer contributions at six Fin-4 slots; explicitZ is a pattern-matched Int table on those same slots (sample entries 4, -2, ...).
The local setting is pure finite enumeration: every index runs over Fin 4, so the identity is a finite family of integer equations. Upstream, the two defs fix the left- and right-hand sides; no analytic continuum limit is taken here.
Downstream assembly will case-split all six indices and invoke one cell theorem per tuple. This declaration is the cell for (2,1,2,3,0,1).
proof idea
One-line kernel proof: by decide. Lean reduces both sides to concrete integers (the fold of couplingZList versus the matched explicitZ entry times 8) and checks equality by the decidable instance on Int. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 arguments by exhaustive fin_cases and discharges each branch with a chunk cell such as this one. That global equality is the algebraic core of the ReggeExactMidpoint M2TT identity in 4D gravity analysis inside the monolith.
Within Recognition Science gravity work, certifying the discrete midpoint numerator against the explicit kernel is bookkeeping needed before continuum or continuum-limit claims; it does not itself invoke the forcing chain (T5–T8), RCL, or phi-ladder mass formulas. It closes one of 256 decide cells so the assemble proof stays sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.