e_302113
plain-language theorem explainer
At multi-index (3,0,2,1,1,3), the folded Regge midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D midpoint M2=8Z identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,0,2,1,1,3)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer kernels are compared pointwise on $(\mathrm{Fin},4)^6$. The numerator $m_2$ is defined by folding a fixed coupling list: each term contributes an integer contrib and the fold starts at 0. The comparison target explicitZ is a closed-form pattern match on the six indices, returning small integers such as $4$, $-2$, and so on.
This module is chunk 12 of the case split that asserts $m_2=8Z$ everywhere. The local setting is purely combinatorial: no continuum limit, only exact integer identities on a finite index set. Upstream, both sides of the equality are the kernel definitions from ReggeExactMidpointM2TTIdentity4DKernelCert.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values at the fixed indices $(3,0,2,1,1,3)$: the left via the fold definition of $m_2$, the right via the pattern match for $Z$ scaled by 8. The kernel checks integer equality and closes the goal.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2=8Z$ and discharges the universal claim by exhaustive fin_cases on all six indices. Each chunk lemma such as this one is an atomic witness that a single cell of the $4^6$ table matches.
In the gravity stack this identity is bookkeeping for the exact midpoint Regge kernel in 4D: once $m_2=8Z$ is global, later curvature and mass-side arguments can quote the closed form $Z$ in place of the folded sum. It is not itself a forcing-chain step (T0–T8); it is infrastructure under the discrete gravity side of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.