e_330323
plain-language theorem explainer
At multi-index (3,3,0,3,2,3) on (Fin 4)^6, the folded coupling numerator m2Num equals eight times the explicit integer table explicitZ. Gravity analysts cite it as one atomic case of the 4D Regge midpoint M2TT numerator identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,3,0,3,2,3)$ in $(\mathrm{Fin}\,4)^6$, the summed coupling numerator equals eight times the explicit closed-form integer at those indices: $N(3,3,0,3,2,3)=8\,Z(3,3,0,3,2,3)$.
background
This module is chunk 15 of a 256-way case split proving that the 4D Regge exact-midpoint M2TT numerator agrees with an explicit integer table, scaled by eight. The ambient setting is discrete gravity analysis: couplings on a 4-index simplex structure with values in Fin 4.
The numerator m2Num a b c d i j is defined by folding a fixed coupling list and summing a local contribution at each term. The comparison object explicitZ is a total function (Fin 4)^6 → ℤ given by an exhaustive pattern table (sample entries include 4, −2, and so on).
The local claim is only the single lattice point with coordinates (3,3,0,3,2,3). Sibling chunks cover the remaining points; the module header states the global goal as m2Num = 8·explicitZ via 256 kernel decides.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left by evaluating the fold that defines the numerator at the fixed six-tuple, the right by looking up the explicit table and multiplying by 8. Lean’s kernel decision procedure discharges the resulting numeral equality with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every (a,b,c,d,i,j) : Fin 4 by exhausting all six indices. That global equality is the certified numerator half of the Regge exact-midpoint M2TT identity in 4D, inside the Gravity analysis stack of the Recognition Science mirror.
The chunk exists so the full identity is a finite, machine-checked case split rather than an opaque closed-form argument. It does not itself invoke the forcing chain (T0–T8), RCL, or φ-ladder mass formulae; those enter only at higher layers that consume the assembled 4D identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.