e_231102
plain-language theorem explainer
For the multi-index (2,3,1,1,0,2) on Fin 4, the folded Regge numerator m2Num equals eight times the closed-form explicitZ value. 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 $a=2$, $b=3$, $c=1$, $d=1$, $i=0$, $j=2$ with each index in $\{0,1,2,3\}$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the M2 TT identity is checked by comparing a folded numerator against a closed-form integer kernel. The numerator m2Num is defined by folding couplingZList and summing each term's contribution contrib at a six-tuple of Fin-4 indices. The comparison target explicitZ is a pattern-matched integer table on those same indices (sample entries include 4 on diagonal-like pairs and -2 on mixed pairs).
This module is chunk 11 of the 256-case kernel decide campaign stated in the module doc: prove m2Num = 8 · explicitZ pointwise. The local setting is pure integer arithmetic on Fin 4; no continuum limit or physical units enter the statement.
proof idea
One-line proof by decide. Lean reduces both sides at the concrete indices (2,3,1,1,0,2): the fold that defines the numerator and the pattern match that defines explicitZ evaluate to integers, and the kernel checks equality with the factor 8. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in Fin 4 and discharges the cases by exhaustive fin_cases. Each chunk lemma such as this one pins one of the 256 kernel points so the assembly can quote a proved equality rather than re-decide the whole table in one place.
Inside Recognition gravity, the midpoint M2 TT identity is part of the discrete curvature bookkeeping that supports the Regge-side consistency checks. The factor 8 is the structural multiplicity relating the folded coupling sum to the explicit kernel; establishing it pointwise is scaffolding for the global algebraic identity, not a continuum GR theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.