e_310220
plain-language theorem explainer
For the concrete multi-index (3,1,0,2,2,0) on Fin 4, the folded coupling numerator m2Num equals eight times the explicit integer table explicitZ. Gravity analysts assembling the 4D Regge midpoint M2 TT identity cite this as one of 256 kernel cases. The proof is a single decide on fully concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,2,2,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-case kernel certification that the numerical mass-squared numerator equals eight times an explicit integer table, in the 4D Regge exact-midpoint M2 TT identity analysis.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add a contribution term for each coupling entry at the six Fin-4 indices. The table $Z$ is an explicit case-split function $\mathrm{Fin},4^6\to\mathbb{Z}$ with hard-coded integer values (e.g. $4$, $-2$) on selected index patterns.
The local goal is pointwise equality $m_2^{\mathrm{num}}=8Z$ at every multi-index; this declaration handles one fixed tuple.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin-4 arguments are literals, so the kernel decision procedure closes the equality with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on all six indices. Each chunk such as this one discharges one concrete branch of that case split.
In the broader Gravity analysis, the identity underwrites the exact midpoint M2 TT kernel certificate for 4D Regge calculus. It is pure integer bookkeeping on the coupling table, not a derivation of continuum Einstein equations, but it is a required algebraic step before continuum or continuum-limit claims can be attached to the discrete kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.