e_311313
plain-language theorem explainer
Finite-case identity: the midpoint mass-squared numerator at multi-index (3,1,1,3,1,3) equals eight times the explicit 4D kernel entry. Gravity analysts assembling the Regge exact midpoint M₂ TT identity cite this cell. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(3,1,1,3,1,3)\in(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(3,1,1,3,1,3)$ equals $8$ times the explicit kernel value $Z(3,1,1,3,1,3)$.
background
In the 4D Regge midpoint analysis, the mass-squared numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at six Fin-4 indices, and the fold starts from 0. The companion table explicitZ is a closed-form integer kernel on the same six indices (sample values include $4$, $-2$, and so on for distinguished index patterns).
This module is chunk 13 of the 256-cell kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The local setting is pure integer arithmetic on a finite index set; no continuum limit or variational argument is invoked here. Upstream, both $m_2^{\mathrm{num}}$ and $Z$ are supplied by the KernelCert module as total functions Fin 4 → ⋯ → Int.
proof idea
One-line kernel proof: decide evaluates both sides at the concrete sextuple $(3,1,1,3,1,3)$ and checks integer equality. No lemmas are invoked beyond the computable definitions of the fold m2Num and the pattern-matched table explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the full pointwise identity
$\forall a,b,c,d,i,j:\mathbb{F}_4,; m_2^{\mathrm{num}}(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$
by exhaustive fin_cases on the six indices. Each chunk lemma such as this one discharges one concrete cell of that case tree.
In the broader Recognition gravity stack, the identity certifies that the midpoint Regge M₂ TT kernel collapses to an explicit sparse table, which is the algebraic input to later continuum and continuum-limit comparisons. It does not itself touch the forcing chain (T0–T8) or the J-cost; it is infrastructure inside the 4D discrete gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.