e_033032
plain-language theorem explainer
For the six Fin-4 indices (0,3,3,0,3,2), the summed coupling numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic case in the exhaustive 4D Regge midpoint M2TT identity. The proof is a single kernel decide on integer arithmetic.
Claim. With $m_2^{\mathrm{num}}$ the fold of coupling contributions over the fixed coupling list and $Z_{\mathrm{ex}}$ the explicit integer kernel on six indices in $\mathrm{Fin}\,4$, one has $m_2^{\mathrm{num}}(0,3,3,0,3,2)=8\,Z_{\mathrm{ex}}(0,3,3,0,3,2)$.
background
The module sits in the 4D Regge-calculus analysis of the exact midpoint M2TT identity. Indices run in $\mathrm{Fin},4$ (four discrete directions). The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed list of coupling terms: each term contributes an integer via a local contrib rule, and the fold starts at 0.
The comparison target explicitZ is a piecewise integer function on the same six indices, with finitely many nonzero patterns (e.g. value 4 on diagonal-type pairs, $-2$ on selected off-diagonal pairs). The local claim of this file is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{ex}}$, discharged in 256-case chunks by kernel decision.
proof idea
One-line proof: by decide. Lean’s decision procedure evaluates both sides as concrete integers (the fold that defines m2Num at the fixed indices, and the matching clause of explicitZ) and checks equality. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. This declaration is the atomic witness for the single multi-index $(0,3,3,0,3,2)$ inside chunk 3 of that case split.
In the broader Recognition gravity stack, the identity certifies that the discrete midpoint curvature numerator matches the closed-form kernel used in the 4D Regge analysis. It is pure finite combinatorics: no continuum limit, no phi-ladder mass formula, and no appeal to the T0–T8 forcing chain beyond the ambient discrete geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.