e_020203
plain-language theorem explainer
For the six-index slot (0,2,0,2,0,3) on Fin 4, the folded numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts cite it when discharging one cell of the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,2,0,3)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-cell kernel certification that the 4D Regge exact-midpoint numerator agrees with eight times a closed-form integer table. The ambient setting is discrete gravity analysis: couplings on oriented 4-simplices are reduced to integer arithmetic on six Fin-4 indices.
The numerator m2Num is defined by folding a fixed coupling list and summing a local contribution at each tuple. The comparison target explicitZ is a pattern-matched integer table on the same six indices (nonzero only on a sparse set of pairings such as $(0,0,1,1,2,2)\mapsto 4$ and sign-flipped off-diagonal slots).
The local claim is one concrete cell of the identity $m_2^{\mathrm{num}}=8Z$, not the quantified statement.
proof idea
One-line computational proof: by decide. Both sides reduce to closed integers once the six Fin-4 arguments are substituted, so the kernel equality checker discharges the goal with no lemmas or case splits inside this declaration.
why it matters
Parent assembly theorem m2Num_eq_eight_explicitZ quantifies over all six Fin-4 indices and proves $m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases. Each chunk theorem such as this one supplies a single decided cell that the case tree lands on.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge curvature weights in 4D, not a new dynamical law. It sits downstream of the kernel certificate definitions and upstream of any global statement that the discrete M2TT numerator matches the explicit table everywhere. No forcing-chain landmark (T5–T8, RCL, phi) is touched; the result is pure finite arithmetic support for the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.