e_310102
plain-language theorem explainer
At multi-index (3,1,0,1,0,2) the folded coupling numerator equals eight times the explicit integer kernel value. Gravity analysts building the 4D Regge midpoint M2 TT identity cite this as one concrete kernel check among the 256-point case split. The proof is a single decide on the evaluated integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,1,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 256-point kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ on every 6-tuple of $\mathrm{Fin},4$ indices. The setting is the exact midpoint analysis of the 4D Regge M2 TT identity in the Gravity.Analysis stack.
The 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 comparison target $\mathrm{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern match (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
Both definitions live in the KernelCert module; this chunk only evaluates them at one concrete multi-index.
proof idea
One-line computational proof: decide. After substituting the concrete Fin 4 literals, both sides reduce to closed integer expressions (fold of contrib versus the matched explicitZ clause, scaled by 8), and the kernel decides equality.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8\cdot Z$ and discharges the claim by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one point of that case tree (chunk 13 of the 256 kernel decides).
In the broader Recognition gravity stack, the identity underwrites the exact midpoint form of the 4D Regge M2 TT kernel used in discrete curvature bookkeeping. It is pure integer algebra on the certified kernel table, not a continuum GR derivation, and does not itself invoke the T0–T8 forcing chain or the J-cost RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.