e_320021
plain-language theorem explainer
For the six Fin-4 indices (3,2,0,0,2,1), the discrete midpoint mass numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the full Regge midpoint M2-TT identity cite this as one of 256 kernel cells. The proof is a pure decide on the evaluated integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(3,2,0,0,2,1)$ equals $8$ times the explicit integer kernel $Z(3,2,0,0,2,1)$.
background
In the Regge exact-midpoint analysis for 4D gravity, two integer-valued kernels on six Fin-4 indices are compared cellwise. The numerator $m_2^{\mathrm{num}}$ is obtained by folding a fixed coupling list: each term contributes an integer via a local contribution function, and the fold starts at zero. The comparison target explicitZ is a sparse pattern-matched table of small integers (typically $\pm 2,\pm 4$, or zero off the listed patterns).
The ambient module is one of many chunks that discharge the identity $m_2^{\mathrm{num}}=8\cdot Z$ by kernel decision rather than by symbolic algebra. Chunk 14 covers a block of the $4^6=4096$ formal cells; only the nonzero or nontrivial cells need named theorems, and this declaration is the cell with indices $(3,2,0,0,2,1)$.
proof idea
One-line kernel decision: both sides are closed integer expressions once the six concrete Fin-4 values are substituted, so decide evaluates $m_2^{\mathrm{num}}(3,2,0,0,2,1)$ via the fold definition and $8\cdot Z(3,2,0,0,2,1)$ via the pattern table and checks equality in $\mathbb{Z}$. No intermediate lemmas are invoked beyond the two definitions.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts the identity for every sextuple of Fin-4 indices by exhaustive fin_cases. Each concrete cell such as this one is a leaf of that case split; without the cell theorems the assembler cannot close. In the broader Recognition gravity stack, the factor-of-eight relation between the folded midpoint numerator and the explicit Z-kernel is the algebraic certificate that the discrete Regge midpoint curvature matches the continuum TT projector structure used downstream. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it is infrastructure for the 4D geometric side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.