e_012222
plain-language theorem explainer
For the six-index slot (0,1,2,2,2,2) 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 M2TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(0,1,2,2,2,2)$ equals eight times the explicit integer kernel at the same slot: $N(0,1,2,2,2,2)=8\,Z(0,1,2,2,2,2)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification. The local goal, stated in the module header, is to prove that the folded numerator equals eight times an explicit integer kernel on a block of the $4^6$ index space (256 decides per chunk).
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add a contribution for each coupling term at the six Fin-4 indices. The explicit kernel $Z$ is a pure pattern-match table on those same six indices, returning small integers such as $4$, $-2$, and so on for the nonzero patterns.
The present declaration fixes one concrete sextuple $(0,1,2,2,2,2)$ inside chunk 1. Sibling lemmas cover the neighboring slots; the full universal statement is assembled downstream by exhaustive fin_cases.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold of contributions at the fixed indices, the right-hand side multiplies the table value of the explicit kernel by 8. Lean’s kernel decision procedure checks the integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by casing through all Fin-4 indices and invoking one chunk lemma per cell. That identity is the algebraic core of the exact midpoint M2TT certification in the 4D Regge gravity analysis stack: it replaces a folded coupling sum by a sparse closed-form kernel, enabling exact (not approximate) midpoint identities used in the discrete gravity sector of Recognition Science.
Within the broader RS gravity program this is bookkeeping infrastructure rather than a forcing-chain landmark (T0–T8). It closes one cell of the finite case split that makes the 4D kernel identity machine-checkable end to end.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.