e_312313
plain-language theorem explainer
For the six-index tuple (3,1,2,3,1,3) on Fin 4, the folded Regge midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=3$, $b=1$, $c=2$, $d=3$, $i=1$, $j=3$ in $\{0,1,2,3\}$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8\,Z_{\mathrm{ex}}(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer via a local contrib rule, and the fold starts at 0. The comparison target $Z_{\mathrm{ex}}$ is an explicit piecewise integer table on the same six indices (sample entries include $4$, $-2$, and other small constants on distinguished patterns).
This module is chunk 13 of a 256-way case split that discharges $m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ pointwise. The local setting is pure finite enumeration: every index lives in Fin 4, so each concrete sextuple is a closed integer identity.
proof idea
One-line computational proof: decide evaluates both sides on the fixed sextuple $(3,1,2,3,1,3)$. The left side runs the fold that defines $m_2^{\mathrm{num}}$; the right side looks up $8\cdot Z_{\mathrm{ex}}$ at those indices. No lemmas beyond the two kernel definitions are required.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the identity for all $a,b,c,d,i,j:\mathrm{Fin},4$ and proves it by nested fin_cases, each leaf a chunk equality of this form. This declaration is the leaf for $(3,1,2,3,1,3)$. Together the chunks certify that the folded midpoint numerator is exactly eight times the explicit kernel, a numerical identity used in the broader Regge M2–TT midpoint analysis in the Gravity domain. It does not itself touch the T0–T8 forcing chain; it is infrastructure for discrete gravity identities inside RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.