e_312032
plain-language theorem explainer
For the multi-index (3,1,2,0,3,2), the folded Regge numerator equals eight times the explicit kernel table entry. Gravity analysts certifying the 4D midpoint M2TT identity cite this as one cell in the 256-point kernel sweep. Proof is a single decide on concrete integer arithmetic from the two definitions.
Claim. The folded coupling numerator at indices $(3,1,2,0,3,2)$ equals eight times the explicit integer kernel at those same indices: $m_2^{\mathrm{num}}(3,1,2,0,3,2)=8\,Z(3,1,2,0,3,2)$.
background
In the 4D Regge exact-midpoint analysis, two integer kernels on six indices drawn from $\mathrm{Fin},4$ are compared pointwise. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer via a local contrib rule, summed from zero. The explicit kernel $Z$ is a closed pattern-match table returning small integers (typical values $4$, $-2$, and so on) on those six indices.
This module is chunk 13 of a 256-cell decide sweep whose sole job is to check $m_2^{\mathrm{num}}=8Z$ at every multi-index. Upstream, only the two definitions are needed; no analytic lemma intervenes. The local setting is pure discrete bookkeeping inside the gravity analysis stack, not a continuum curvature identity.
proof idea
One-line computational wrapper: decide evaluates both sides as concrete Int values. The left-hand side runs the fold that defines the numerator at $(3,1,2,0,3,2)$; the right-hand side multiplies the matched explicit-kernel clause by eight. Kernel reduction confirms the integers agree. No named lemmas beyond the two definitions are applied.
why it matters
Downstream, the assembly theorem m2Num_eq_eight_explicitZ states the universal claim $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges it by fin_cases on all six $\mathrm{Fin},4$ indices; each branch lands on a cell theorem such as this one. That universal equality is part of the Regge exact-midpoint M2TT identity certification in 4D. Within Recognition Science gravity work it is scaffolding for exact discrete curvature bookkeeping on the $D=3$ spatial scaffold, not itself a forcing-chain (T0–T8) step. It closes one of 256 decide obligations in chunk 13.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.