e_321311
plain-language theorem explainer
For the six-index tuple (3,2,1,3,1,1) on Fin 4, the folded numerical m₂ coupling equals eight times the explicit integer kernel Z. Gravity analysts assembling the full Regge midpoint identity cite this as one of the 256 kernel cells. The proof is a single decide on concrete integers.
Claim. For indices $a{=}3,b{=}2,c{=}1,d{=}3,i{=}1,j{=}1$ in $\{0,1,2,3\}$, the numerical midpoint coupling satisfies $m_2^{\mathrm{num}}(3,2,1,3,1,1)=8\,Z_{\mathrm{expl}}(3,2,1,3,1,1)$, where $m_2^{\mathrm{num}}$ is the fold of coupling contributions and $Z_{\mathrm{expl}}$ is the closed-form integer table.
background
In the 4D Regge exact-midpoint analysis, the numerical second-moment coupling $m_2^{\mathrm{num}}$ is defined by folding a fixed list of coupling terms: each term contributes an integer depending on six Fin-4 indices $(a,b,c,d,i,j)$. The companion table $Z_{\mathrm{expl}}$ is an explicit piecewise integer function on the same six indices (sample values include $\pm 2,,4$ on diagonal and off-diagonal patterns).
The local module is chunk 14 of a 256-cell kernel certification: the claim under audit is one concrete cell of the identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$. The ambient goal is a fully decided algebraic identity for the Regge midpoint mass/TT sector in four dimensions, with no analytic remainder.
proof idea
One-line computational discharge: decide evaluates both sides at the fixed indices $(3,2,1,3,1,1)$. The left side runs the fold that defines $m_2^{\mathrm{num}}$; the right side looks up $Z_{\mathrm{expl}}$ and multiplies by 8. Equality of the resulting integers is decided in the kernel. No lemmas beyond the two definitions are invoked.
why it matters
This cell is consumed by the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases over all six Fin-4 arguments, routing each branch to a chunk equality of this form.
In the Recognition gravity stack, the identity closes the numerical side of the Regge midpoint TT/mass kernel in 4D, so downstream curvature and continuum-limit arguments can quote a single global factor-of-eight relation rather than a fold. It is pure certification scaffolding inside the Gravity.Analysis layer, not a forcing-chain (T0–T8) step, but it underwrites the discrete geometric side that those continuum claims eventually rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.