e_313302
plain-language theorem explainer
Pointwise identity: the folded coupling numerator m2Num at multi-index (3,1,3,3,0,2) equals eight times the explicit integer kernel explicitZ at the same indices. Gravity analysts cite it only as one cell of the 4D Regge midpoint M2TT numerator identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,3,0,2)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit integer kernel value: $N(3,1,3,3,0,2)=8\,Z(3,1,3,3,0,2)$.
background
In the 4D Regge exact-midpoint M2TT analysis, two integer kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $N=\mathrm{m2Num}$ 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 $Z=\mathrm{explicitZ}$ is a closed-form piecewise integer table on the same six indices (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
This module is chunk 13 of the exhaustive pointwise certification that $N=8Z$ everywhere. The local setting is pure finite enumeration: 256 decide obligations in the chunk, each fixing one multi-index.
proof idea
One-line computational proof: decide. Lean reduces both sides at the concrete sextuple $(3,1,3,3,0,2)$ to integers (the fold for $N$, the matching clause or default for $Z$) and checks equality. No lemmas beyond the two kernel definitions are invoked.
why it matters
Feeds the assembly theorem $\mathrm{m2Num_eq_eight_explicitZ}$, which states $\forall a,b,c,d,i,j,,N=8Z$ and discharges the claim by six nested $\mathrm{fin_cases}$, each leaf a chunk theorem of this form. That global identity is the algebraic core of the Regge exact-midpoint M2TT numerator certification in 4D gravity analysis inside the monolith. It does not itself touch the T0–T8 forcing chain, $\phi$-ladder masses, or $\alpha$; it is infrastructure for the discrete curvature/coupling bookkeeping those layers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.