e_020022
plain-language theorem explainer
For the six-index slot (0,2,0,0,2,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these micro-identities when assembling the global Regge midpoint M2–TT identity in 4D. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(0,2,0,0,2,2)$ equals eight times the explicit integer kernel at the same slot: $N(0,2,0,0,2,2)=8\,Z(0,2,0,0,2,2)$.
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 check $N=8Z$ on a block of the $4^6$ index space by kernel decision rather than by symbolic expansion.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start from $0$ and add a contribution term for each coupling triple at the six Fin-4 indices. The comparison target $Z=\mathrm{explicitZ}$ is a closed integer table on those same six indices (nonzero only on a sparse set of patterns such as $(0,0,1,1,2,2)\mapsto 4$ and various $-2$ off-diagonal slots).
Chunk 2 holds a family of sibling equalities of the same shape, one per concrete index tuple. Together they feed the exhaustive case split that proves the identity for every index.
proof idea
One-line proof by decide. Both sides are closed integer expressions once the six Fin-4 arguments are literals: the left side evaluates the fold of contrib over couplingZList, the right side multiplies the pattern-matched explicitZ entry by 8. Lean’s kernel decision procedure discharges the resulting numeral equality with no lemmas and no case split inside this declaration.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts $\forall a,b,c,d,i,j,, N=8Z$ on Fin 4. Its proof is pure fin_cases over all six indices; each leaf is one of these chunk theorems. This declaration is the leaf for $(0,2,0,0,2,2)$.
In the gravity analysis stack, the identity $N=8Z$ is the algebraic core of the Regge exact-midpoint M2–TT certification in 4D: it converts a folded coupling sum into an explicit sparse integer kernel that can be matched against the continuum TT projector structure. Without the chunk leaves, the assemble theorem cannot close.
No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; the result is pure discrete tensor algebra supporting the RS gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.