e_103302
plain-language theorem explainer
For the six Fin-4 indices (1,0,3,3,0,2), the discrete midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel cases. The proof is a single kernel decide on the concrete integer equality.
Claim. For indices $a{=}1,\,b{=}0,\,c{=}3,\,d{=}3,\,i{=}0,\,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 $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the discrete second-moment numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The companion map $Z$ is an explicit pattern-matched integer on six $\mathrm{Fin},4$ indices (examples: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$).
This module is chunk 4 of the exhaustive verification that $m_2^{\mathrm{num}}=8Z$ on every index tuple. The local setting is pure integer arithmetic over a finite discrete kernel; no continuum limit is taken here. Upstream, both $m_2^{\mathrm{num}}$ and $Z$ live in the KernelCert module that supplies the coupling list and the closed form.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides of the concrete equality $m_2^{\mathrm{num}}(1,0,3,3,0,2)=8\cdot Z(1,0,3,3,0,2)$ as integers and closes the goal. No lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and $Z$ are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,, m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one branch of that case split. The identity is the algebraic core of the exact midpoint M2TT relation in the 4D Regge gravity analysis: once numerator and explicit kernel match everywhere, the continuum-facing midpoint formula can quote a fully certified discrete factor of eight rather than a residual sum. It does not itself touch the forcing chain T0–T8 or the Recognition Composition Law; it is infrastructure inside the gravity discrete-kernel layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.