e_011230
plain-language theorem explainer
For the six-index slot (0,1,1,2,3,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the exact midpoint M2 TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}1$, $d{=}2$, $i{=}3$, $j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,1,1,2,3,0)=8\,Z(0,1,1,2,3,0)$.
background
This module is chunk 1 of a 256-case kernel certification that the 4D Regge midpoint numerator equals eight times a sparse explicit table. Indices run over $\mathrm{Fin},4$, labeling discrete directions in the 4-simplex / TT sector.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each local contribution at those six indices. The companion table $Z$ is an explicit pattern-match on the six $\mathrm{Fin},4$ arguments, returning small integers (e.g. $\pm 2,4$) on the supported patterns and (implicitly) zero elsewhere.
The local claim is one concrete six-tuple in that table: $(0,1,1,2,3,0)$. Sibling lemmas cover the other tuples in the same chunk; the assemble theorem quantifies over all of $\mathrm{Fin},4^6$.
proof idea
One-line decide proof. Both sides reduce to concrete Int values: the left by evaluating the fold of contributions at the fixed indices, the right by multiplying the pattern-matched explicitZ entry by 8. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases on all six indices. That identity is the algebraic core of the exact midpoint M2 TT certification in 4D Regge gravity analysis inside the monolith.
In the broader Recognition Science gravity stack, such exact discrete identities pin the curvature/TT sector before continuum or phenomenological limits. This chunk entry is pure bookkeeping: one of 256 decides that close the case split. It does not itself invoke the forcing chain (T0–T8), RCL, or $\phi$-ladder mass formulae; it is infrastructure under the Regge exactness claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.