e_313332
plain-language theorem explainer
For the six-index tuple (3,1,3,3,3,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity in 4D cite this as one of the 256 kernel cells. The proof is a single decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}1$, $c{=}3$, $d{=}3$, $i{=}3$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-cell kernel certification that the Regge midpoint mass-squared numerator equals eight times an explicit integer table on six Fin-4 indices. The ambient setting is 4D discrete gravity analysis for the exact midpoint M2 TT identity.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add a contribution term for each coupling entry at the six indices. The companion table $Z$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by exhaustive pattern match (typical nonzero values are $\pm 2,\pm 4$).
The global claim is $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$. Each chunk theorem discharges one concrete six-tuple so the assembler can finish by fin_cases.
proof idea
One-line kernel cell: decide evaluates both sides as concrete Int values. The left side runs the fold of m2Num on the fixed coupling list at indices $(3,1,3,3,3,2)$; the right side multiplies the pattern-matched explicitZ entry by 8. No lemmas are invoked beyond decidable equality of integers.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $\mathrm{Fin},4$ by exhaustive fin_cases and cites each chunk cell. That global equality is the algebraic backbone of the Regge exact-midpoint M2 TT identity certification in 4D gravity analysis inside the monolith.
In the Recognition Science gravity stack this is bookkeeping, not a new physical law: it locks the discrete curvature/mass-squared numerator to a sparse explicit kernel so later continuum or continuum-limit arguments can quote a proved integer identity rather than a schematic fold. It does not itself invoke the forcing chain (T5–T8), RCL, or the $\varphi$-ladder; those enter only if downstream gravity theorems import this certified kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.