e_320201
plain-language theorem explainer
For the six-index tuple (3,2,0,2,0,1) on Fin 4, the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts assembling the 4D Regge exact-midpoint M2TT identity cite this as one of the 256 kernel cases. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}2$, $c{=}0$, $d{=}2$, $i{=}0$, $j{=}1$ 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 chunk 14 of a 256-case kernel certification that the midpoint numerator of the 4D Regge M2TT identity is exactly eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, matching the four spacetime directions of the discrete geometry.
Upstream, $\mathrm{m2Num}$ is defined by folding a coupling list: it sums contribution terms $\mathrm{contrib},t,a,b,c,d,i,j$ over every coupling token $t$. The companion table $\mathrm{explicitZ}$ is a pattern-matched integer function on six $\mathrm{Fin},4$ arguments, returning small constants such as $4$, $-2$, and (implicitly) $0$ off the listed patterns.
The local claim is the pointwise identity at one concrete six-tuple. Sibling lemmas cover the other index combinations in the same chunk.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold that defines the numerator at $(3,2,0,2,0,1)$, the right-hand side multiplies the table lookup by eight. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the universal statement $\mathrm{m2Num_eq_eight_explicitZ}$, which introduces all six $\mathrm{Fin},4$ indices and discharges them by nested fin_cases, routing each branch to a chunk lemma of this form. That universal equality is the algebraic core of the Regge exact-midpoint M2TT identity in 4D discrete gravity analysis inside the Recognition Science gravity stack.
In the broader framework this sits under the gravity domain that ultimately supports continuum limits consistent with $D=3$ spatial dimensions (forcing step T8) and the discrete causal structure. It does not itself touch the J-cost or phi-ladder mass formula; it is pure kernel arithmetic closing one cell of the 256-case table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.