e_001032
plain-language theorem explainer
At multi-index (0,0,1,0,3,2), the folded Regge numerator equals eight times the explicit integer kernel entry. Gravity analysts certifying the 4D midpoint M2TT identity cite this as one of 256 finite-case certificates. The proof is a single kernel decide on concrete integers after unfolding both sides.
Claim. For indices $(a,b,c,d,i,j)=(0,0,1,0,3,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(0,0,1,0,3,2)=8\,Z(0,0,1,0,3,2)$.
background
In the 4D Regge exact-midpoint analysis, two integer kernels live on six indices each ranging in $\mathrm{Fin},4$. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start from $0$ and add a contribution term at each coupling triple for the given indices. The companion table $Z$ is an explicit sparse function $\mathrm{Fin},4^6\to\mathbb{Z}$ listing the closed-form kernel values case by case.
The local module is chunk 0 of a 256-way case split that certifies the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ by kernel decision on each multi-index. Upstream, both $m_2^{\mathrm{num}}$ and $Z$ are supplied by the KernelCert module; this declaration only evaluates them at the fixed tuple $(0,0,1,0,3,2)$.
proof idea
One-line wrapper: decide evaluates both sides as concrete Int expressions. Unfolding the fold that defines the numerator and the match that defines the explicit kernel reduces the goal to a numeric equality, which the kernel closes.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges it by exhaustive fin_cases on all six indices. Each residual goal is exactly one chunk certificate of this form; the present lemma is the residual for $(0,0,1,0,3,2)$.
Within Recognition Gravity, the Regge midpoint M2TT block is analytic scaffolding for the discrete curvature side of the forcing chain (spatial $D=3$ already fixed at T8). Closing the numerator-versus-explicit-kernel identity removes a large case-bash obligation from the 4D assembly path. No continuum or phenomenological claim is made here; the lemma is pure finite arithmetic support for that assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.