e_223113
plain-language theorem explainer
For the multi-index (2,2,3,1,1,3) on Fin 4, the folded coupling numerator equals eight times the tabulated explicit kernel integer. Gravity analysts cite it when assembling the full Regge midpoint M2TT identity over all 4^6 index sextuples. The proof is a single kernel decide on a closed integer equality.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(2,2,3,1,1,3)$. Then the summed coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 10 of a 256-case kernel certification that the Regge-exact midpoint numerator equals eight times an explicit integer table on every sextuple of indices in $\mathrm{Fin},4$.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at $0$ and add each triple's contribution at the six indices. The table $Z=\mathrm{explicitZ}$ is a pattern-matched $\mathrm{Fin},4^6\to\mathbb{Z}$ map with sparse nonzero entries (e.g. $4$ on diagonal-like pairs, $-2$ on crossed pairs).
The local claim is one concrete sextuple in that exhaustive grid. Upstream, only the two definitions are needed; no analytic lemma intervenes.
proof idea
One-line computational proof: decide evaluates both sides as concrete integers (the fold of m2Num at $(2,2,3,1,1,3)$ and $8\cdot Z(2,2,3,1,1,3)$) and checks equality in the kernel. No rewriting or case split appears in this chunk.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; N=8Z$ by exhausting all six indices with fin_cases. Each chunk theorem such as this one discharges one leaf of that $4^6$ tree.
In the Recognition gravity stack this identity is bookkeeping for the Regge-exact midpoint form of the M2TT kernel in 4D: once numerator and explicit table match by the factor eight everywhere, later curvature and continuum-limit arguments can quote a single closed expression rather than a fold. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is pure discrete kernel algebra supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.