e_120300
plain-language theorem explainer
For the multi-index (1,2,0,3,0,0) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel value. Gravity analysts certifying the 4D Regge midpoint M2TT identity cite this as one cell of the 256-case grid. The proof is a single kernel decide on the concrete integer arithmetic.
Claim. For $a=1$, $b=2$, $c=0$, $d=3$, $i=0$, $j=0$ 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 exact-midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: it sums a contribution function at six indices in $\mathrm{Fin},4$. The companion explicit kernel $Z$ is a sparse integer table (values such as $\pm 2$, $\pm 4$, or $0$) giving the closed form at the same indices.
This module is chunk 6 of a 256-case certification that $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. Both sides are defined in the KernelCert import; the chunk only discharges one concrete sextuple by computation.
proof idea
One-line computational proof. The tactic decide evaluates both sides as concrete integers (the fold that defines the numerator, and the match that defines the explicit kernel) and checks equality in the kernel. No lemmas are invoked beyond that decision procedure.
why it matters
The parent theorem is the assembled pointwise identity: for all six $\mathrm{Fin},4$ indices, the numerator equals eight times the explicit kernel. That proof introduces the indices and runs fin_cases on each, landing on chunk lemmas such as this one. The identity is bookkeeping inside the Regge exact-midpoint M2TT certification in the gravity stack; it closes one cell of the decide grid rather than stating a new continuum law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.