e_312213
plain-language theorem explainer
For the Fin-4 index tuple (3,1,2,2,1,3), the discrete coupling numerator m2Num equals eight times the closed-form kernel explicitZ. Analysts assembling the exact 4D Regge midpoint M2TT identity cite this as one atomic case among the 4^6 kernel. The proof is a single native decide that evaluates both integer sides.
Claim. For indices $a=3$, $b=1$, $c=2$, $d=2$, $i=1$, $j=3$ in $\{0,1,2,3\}$, the summed coupling numerator equals eight times the explicit integer kernel value: $m_2^{\mathrm{num}}(3,1,2,2,1,3)=8\,Z_{\mathrm{expl}}(3,1,2,2,1,3)$.
background
In the 4D Regge midpoint analysis, the M2TT identity reduces a discrete second-moment numerator built from edge couplings to a simple multiple of an explicit integer kernel on six indices drawn from Fin 4.
The numerator folds a fixed coupling list, accumulating integer contributions at each six-tuple. Its companion explicitZ is a piecewise Int-valued table on the same indices (sample clauses return values such as 4 or -2).
This module is chunk 13 of a 256-way split of the full $4^6$ kernel: each chunk discharges a block of concrete equalities numerator = 8 · explicitZ by native decision procedures.
proof idea
One-line computational proof. The tactic decide evaluates both sides as concrete integers: the left by folding the coupling list at the fixed indices, the right by matching the piecewise explicitZ table, then checks equality. No intermediate lemmas are invoked beyond the two definitions.
why it matters
Feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which asserts the same identity for every six-tuple in Fin 4 by exhaustive fin_cases. That global equality is the algebraic core of the exact 4D Regge midpoint M2TT identity in the Gravity analysis stack.
Within Recognition Science gravity work, such kernel certificates underwrite discrete curvature identities in the 4D ambient (the forcing chain's T8 fixes three spatial dimensions; spacetime here is the Regge setting). Closes one of the 4096 atomic cases in the chunked decide campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.