e_123032
plain-language theorem explainer
For the six-index tuple (1,2,3,0,3,2) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel value. Gravity analysts cite it as one atomic case in the 256-way certification that the Regge midpoint M2TT numerator matches the closed-form kernel. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=1,b=2,c=3,d=0,i=3,j=2$ 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 entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-case kernel certification that the Regge exact-midpoint M2TT numerator in 4D coincides with eight times a closed-form integer table. The ambient setting is discrete gravity analysis: couplings on oriented 4-simplices reduced to integer arithmetic on $\mathrm{Fin},4$ indices.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing local contributions at a six-index slot. The comparison object is an explicit piecewise integer function $Z$ on $(\mathrm{Fin},4)^6$, tabulated by pattern (e.g. diagonal blocks map to $4$, certain off-diagonal swaps to $-2$). The claim is the pointwise identity at one concrete slot.
proof idea
One-line computational proof: both sides evaluate to concrete integers once the six Fin-4 indices are substituted, and decide discharges the resulting integer equality. No algebraic lemmas are invoked beyond the definitions of the folded numerator and the explicit kernel table.
why it matters
Parent assembly theorem m2Num_eq_eight_explicitZ quantifies over all six Fin-4 indices by exhaustive fin_cases, and each leaf is one of these chunk equalities. Without the full 256-case cover, the closed-form replacement of the folded numerator by $8Z$ is not certified. In the Recognition gravity stack this identity is bookkeeping infrastructure for the Regge midpoint M2TT analysis, not a forcing-chain landmark (T0–T8); it simply clears a finite integer identity so later curvature or continuum-limit arguments can quote the explicit kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.