e_330101
plain-language theorem explainer
For the multi-index (3,3,0,1,0,1) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2 TT identity. The proof is a single decide on the concrete integers.
Claim. For indices $a=3$, $b=3$, $c=0$, $d=1$, $i=0$, $j=1$ in $\{0,1,2,3\}$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 15 of a 256-case kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathrm{Fin},4)^6$. The setting is the exact midpoint evaluation of the 4D Regge M2 TT identity used in the gravity analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six indices. The explicit kernel $Z$ is a closed-form integer table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for distinguished index patterns).
The local claim is one concrete sextuple in that table, not the universal statement.
proof idea
One-line computational proof: decide evaluates both sides as concrete Int values (the fold defining the numerator versus eight times the matched explicitZ clause) and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 sextuple by nested fin_cases and needs each atomic equality such as this one. That universal identity is the certified numerator side of the Regge exact-midpoint M2 TT relation in 4D gravity analysis.
Within Recognition Science this sits in the gravity domain supporting continuum limits and discrete curvature bookkeeping; it does not itself touch the T0–T8 forcing chain, RCL, or the phi-ladder mass formula, but it hardens a computational lemma those continuum arguments rely on when they quote the 4D midpoint kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.