e_030320
plain-language theorem explainer
For the six-index slot (0,3,0,3,2,0) on Fin 4, the folded Regge numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D midpoint M2 TT identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $N_2(0,3,0,3,2,0)=8\,Z_{\mathrm{exp}}(0,3,0,3,2,0)$, where $N_2$ is the fold of coupling contributions and $Z_{\mathrm{exp}}$ is the explicit integer kernel table.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator $N_2=\mathrm{m2Num}$ is defined by folding a fixed coupling list: each term contributes an integer via a local contrib rule, and the fold starts at 0. The comparison target $Z_{\mathrm{exp}}=\mathrm{explicitZ}$ is a closed pattern-match table on the same six indices, returning small integers such as $4$, $-2$, and so on for the listed patterns (and implicitly 0 off-pattern).
The module is chunk 3 of a 256-case kernel certification that $N_2=8,Z_{\mathrm{exp}}$ pointwise. The local setting is pure finite enumeration: every index runs in $\mathrm{Fin},4$, so the identity is a finite family of integer equations, split across chunk files for kernel load.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six indices are substituted: the left side evaluates the fold that defines m2Num at $(0,3,0,3,2,0)$; the right side multiplies the table lookup explicitZ at those indices by 8. Lean’s decision procedure discharges the resulting closed integer equality with no lemmas beyond the two definitions.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the full pointwise identity $\forall a,b,c,d,i,j,,N_2=8,Z_{\mathrm{exp}}$ by nested fin_cases on all six indices; each leaf is one of these chunk equalities. This file supplies the leaf for $(0,3,0,3,2,0)$ inside chunk 3.
In the gravity stack the identity is the algebraic certificate that the midpoint M2 TT kernel matches its explicit closed form, a prerequisite for exact Regge curvature bookkeeping in four dimensions. It is computational scaffolding rather than a forcing-chain step (T0–T8), but it locks the discrete curvature numerator used downstream in the RS gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.