e_201031
plain-language theorem explainer
For the six Fin-4 indices (2,0,1,0,3,1), the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one cell of the 256-case grid that certifies the Regge midpoint M2TT identity in 4D. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}0$, $c{=}1$, $d{=}0$, $i{=}3$, $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 8 of a 256-cell decide grid that checks the pointwise identity m2Num = 8·explicitZ on all sextuples of Fin-4 indices. The setting is the 4D Regge midpoint analysis of the M2TT gravitational kernel.
The numerator m2Num(a,b,c,d,i,j) is defined by folding a fixed coupling list: it sums contrib(t,a,b,c,d,i,j) over every term t in couplingZList, yielding an integer. The comparison target explicitZ is a total function Fin 4^6 → ℤ given by an exhaustive pattern match (for example 4 on (0,0,1,1,2,2), −2 on several mixed pairs, and so on).
The parent assembly theorem will quantify over all six indices and discharge the universal claim by fin_cases, each leaf being one of these chunk theorems.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides at the concrete Fin-4 sextuple (2,0,1,0,3,1). The left side reduces by unfolding the foldl over couplingZList and summing the integer contributions; the right side multiplies the matched explicitZ clause by 8. Equality of the resulting integers is decided by the kernel with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states ∀ a b c d i j, m2Num = 8·explicitZ and is proved by six nested fin_cases whose leaves are exactly these chunk decides. That universal identity is the algebraic core of the Regge-exact midpoint M2TT certification in 4D gravity analysis inside the Recognition Science monolith.
In the broader RS gravity stack this closes a finite computational gap: once every cell of the 256-grid is decided, the midpoint kernel is known to match the closed form used downstream in continuum and continuum-limit arguments. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete kernel arithmetic supporting the gravity side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.