e_123121
plain-language theorem explainer
For the concrete six-index tuple (1,2,3,1,2,1) in (Fin 4)^6, the folded Regge coupling numerator equals eight times the explicit integer kernel value. Gravity analysts cite it as one cell of the 256-case kernel table that certifies the midpoint M2TT identity in 4D. The proof is a single kernel decide on the evaluated integers.
Claim. For indices $a{=}1,b{=}2,c{=}3,d{=}1,i{=}2,j{=}1$ in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-cell kernel certification that the 4D Regge midpoint mass-squared numerator equals eight times a closed-form integer table. The ambient setting is exact midpoint analysis of the M2TT identity in discrete gravity on a 4-index simplex labeling.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each list entry's contribution at the six Fin-4 indices. The explicit kernel $Z$ is a pattern-matched integer table on $(\mathrm{Fin},4)^6$ (sample values include $4$, $-2$, and so on for the listed index patterns).
The local claim is only the single cell with indices $(1,2,3,1,2,1)$. Sibling theorems cover the other cells in the same chunk.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple and checks integer equality. No lemmas are invoked beyond the definitions of the folded numerator and the explicit kernel table; the kernel reduces the equality to a true Prop on Int.
why it matters
Parent assembly theorem m2Num_eq_eight_explicitZ states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges it by exhaustive fin_cases on all six indices. Each concrete cell such as this one supplies the residual goal for that branch.
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint Regge analysis in 4D (spatial $D=3$ plus time), not a forcing-chain step. It closes one of the 256 kernel decides named in the module doc, so the assembled equality can be used without residual case obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.