e_032013
plain-language theorem explainer
For the six-index tuple (0,3,2,0,1,3) on Fin 4, the folded coupling numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts cite it as one atomic case of the 4D Regge midpoint M2–TT numerator identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the folded coupling numerator and $Z$ for the explicit integer kernel, one has $N(0,3,2,0,1,3)=8\,Z(0,3,2,0,1,3)$.
background
This module sits in the Gravity analysis stack for the exact midpoint form of a 4D Regge M2–TT identity. The local goal, stated in the module header, is to certify $m2Num=8\cdot explicitZ$ on one 256-case chunk of the six-fold Fin-4 index space by kernel decides.
The numerator $m2Num(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it accumulates integer contributions $contrib,t$ over that list and returns an Int. The comparison target $explicitZ$ is a closed-form Int-valued kernel on $(Fin,4)^6$, specified by pattern-matched cases (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$).
Both definitions live in the KernelCert module imported here. The present declaration fixes one concrete multi-index inside chunk 3 and asserts the scalar identity at that point.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete Fin-4 indices to closed integers (via the fold definition of the numerator and the pattern match for the explicit kernel) and checks equality in the kernel. No lemmas are invoked beyond that reduction.
why it matters
The parent theorem is m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(Fin,4)^6$. Its proof exhausts the index space by fin_cases; each chunk lemma such as this one discharges one concrete cell of that grid.
In the Recognition gravity stack this numerator identity is bookkeeping for the exact midpoint M2–TT comparison in 4D Regge calculus: it guarantees the folded coupling sum matches the closed kernel used downstream. It does not itself touch the forcing chain (T0–T8), RCL, or the phi ladder; it is pure discrete-index algebra supporting the gravity side of the mirror.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.