e_211111
plain-language theorem explainer
For the single multi-index (2,1,1,1,1,1) on Fin 4, the folded numerator coupling m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2TT identity. The proof is a pure kernel decide on the two integer definitions.
Claim. Let $a,b,c,d,i,j \in \{0,1,2,3\}$. Writing $m_2^{\mathrm{num}}$ for the folded integer coupling and $Z$ for the explicit kernel table, one has $m_2^{\mathrm{num}}(2,1,1,1,1,1) = 8\, Z(2,1,1,1,1,1)$.
background
The module sits in the 4D Regge midpoint analysis: one must show that a numerator coupling built by folding a contribution list equals eight times a closed-form integer kernel on every multi-index in $(\mathrm{Fin},4)^6$.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined as the fold of contrib over couplingZList, starting from 0. The companion explicitZ is a pattern-matched table $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample clauses send $(0,0,1,1,2,2)$ to 4 and $(0,0,1,2,1,2)$ to $-2$).
Local setting (module doc): this file is chunk 9 of the 256-decide kernel that discharges $m_2^{\mathrm{num}}=8\cdot Z$ pointwise.
proof idea
One-line proof by decide. Lean reduces both sides of the equality on the concrete six-tuple $(2,1,1,1,1,1)$: the fold that defines $m_2^{\mathrm{num}}$ and the pattern match that defines $Z$, then checks the resulting integers satisfy $n=8z$. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one concrete branch of that case split.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2TT kernel in 4D Regge calculus: once every multi-index matches, the folded coupling may be replaced by the closed table $Z$, simplifying curvature and mass-side identities downstream. It does not itself touch T0–T8 or the RCL; it is pure discrete-geometry algebra inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.