e_210222
plain-language theorem explainer
For the six-index slot (2,1,0,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 M2 TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=1$, $c=0$, $d=2$, $i=2$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(2,1,0,2,2,2)=8\,Z(2,1,0,2,2,2)$.
background
This module is one chunk of a 256-case kernel certification that the 4D Regge midpoint M2 TT numerator equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, matching discrete 4-simplex edge/face labels in the Regge triangulation.
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-matched integer function on the same six $\mathrm{Fin},4$ arguments (nonzero only on a short list of index patterns, with values such as $\pm 2,,4$).
Chunk 9 discharges one concrete sextuple among the $4^6$ combinations; sibling lemmas cover the neighboring slots. The global identity is reassembled downstream by exhaustive fin_cases.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side by evaluating the fold of contributions at the fixed indices $(2,1,0,2,2,2)$, the right-hand side by looking up (or defaulting) the explicit kernel and multiplying by 8. Lean’s kernel decision procedure checks 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 on all six $\mathrm{Fin},4$ indices and invoking one chunk lemma per cell. That global equality is the algebraic core of the exact midpoint M2 TT identity in the 4D Regge gravity analysis stack.
In the Recognition Science gravity line this certifies that the discrete curvature/coupling numerator matches a sparse closed form, so later continuum or continuum-limit comparisons rest on a fully decided finite identity rather than an unexpanded sum. It is pure finite combinatorics: no continuum limit, no forcing-chain step (T0–T8), and no appeal to $J$, $\varphi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.