e_313300
plain-language theorem explainer
For the six-index tuple (3,1,3,3,0,0) on Fin 4, the folded Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3,b{=}1,c{=}3,d{=}3,i{=}0,j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel: $m_2^{\mathrm{num}}(3,1,3,3,0,0)=8\,Z_{\mathrm{explicit}}(3,1,3,3,0,0)$.
background
In the 4D Regge midpoint M2TT analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator m2Num is the fold of a fixed coupling list: it sums contrib t a b c d i j over every term t in couplingZList. The comparison target explicitZ is a piecewise closed form on the same six indices (sample clauses return 4, -2, and so on).
The local module is chunk 13 of the exhaustive case split that asserts m2Num = 8 · explicitZ at every multi-index. The ambient goal is an exact algebraic identity for the midpoint discrete curvature coupling in four dimensions, certified by 256 kernel decisions rather than a symbolic rewrite.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed tuple (3,1,3,3,0,0): the left via the fold definition of m2Num, the right via the matching clause of explicitZ scaled by 8. The kernel checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
This atom is consumed by m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 indices and discharges the goal by nested fin_cases over a,b,c,d,i,j, each leaf a chunk theorem of this form. Closing every leaf certifies the exact midpoint M2 numerator identity used in the discrete gravity analysis. It is pure algebraic bookkeeping inside the Gravity domain, not a forcing-chain (T0–T8) step, but it removes a large case-split obligation from the Regge exact-identity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.