e_312222
plain-language theorem explainer
Pointwise identity: the folded Regge midpoint numerator at multi-index (3,1,2,2,2,2) equals eight times the explicit integer kernel at that same index. Gravity analysts cite it as one cell of the 4D M2–TT kernel certification. The proof is a pure kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,2,2,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit kernel value: $N(3,1,2,2,2,2)=8\,Z(3,1,2,2,2,2)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2–TT identity certification. The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: each term contributes an integer depending on six $\mathrm{Fin},4$ indices, and the fold sums those contributions from zero.
The comparison object $Z=\mathrm{explicitZ}$ is a closed-form integer table on the same six indices (pattern-matched cases such as $(0,0,1,1,2,2)\mapsto 4$ and several $-2$ off-diagonal patterns). The local claim is the scalar relation $N=8Z$ at one concrete multi-index.
Upstream, both $N$ and $Z$ live in the kernel certificate module; this file only discharges individual decide obligations so the global assembly can case-split without recomputing the fold.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(3,1,2,2,2,2)$. The left side runs the fold that defines the numerator; the right side multiplies the table lookup for the explicit kernel by eight. No lemmas are invoked beyond decidable integer equality.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is a leaf of that case tree (module doc: chunk 13 of the 256 kernel decides).
In the gravity stack this identity is bookkeeping for the exact midpoint Regge M2–TT relation in four dimensions: once $N=8Z$ holds pointwise, later arguments may replace the folded coupling sum by the closed kernel table. It does not itself touch the RS forcing chain (T0–T8) or the J-cost; it is infrastructure inside the discrete gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.