e_013120
plain-language theorem explainer
For the six-index tuple (0,1,3,1,2,0) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it when assembling the full 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=3$, $d=1$, $i=2$, $j=0$ in $\{0,1,2,3\}$, the summed coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2–TT identity certification. The local goal, stated in the module header, is to show the folded numerator equals eight times an explicit integer table, case by case, via kernel decides.
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 pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and other small integers on the listed patterns).
Both definitions live in the kernel-certificate module imported here. The present declaration fixes one concrete six-tuple and asserts the scalar identity at that point.
proof idea
One-line proof by decide. Lean reduces both sides to concrete integers: the left-hand side by evaluating the fold of contributions at $(0,1,3,1,2,0)$, the right-hand side by evaluating $8$ times the pattern match for $Z$ at the same indices, then checks equality in the kernel.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the identity for every six-tuple in $(\mathrm{Fin},4)^6$. Its proof is exhaustive fin_cases on all six indices; each leaf is one of these chunk theorems (this module is chunk 1 of the 256-decide split).
Closing the numerator–kernel match is a concrete algebraic step inside the 4D Regge midpoint analysis for the M2–TT sector. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law, but it supplies certified integer arithmetic that those gravity layers rely on when the continuum limit and discrete curvature identities are assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.