e_103113
plain-language theorem explainer
For the multi-index (1,0,3,1,1,3) on Fin 4, the folded Regge coupling numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts cite it as one cell in the 4D midpoint M2–TT identity. The proof is a single decide on the concrete integer equality.
Claim. For indices $a=1$, $b=0$, $c=3$, $d=1$, $i=1$, $j=3$ in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit integer kernel value at that sextuple: $N(1,0,3,1,1,3)=8\,Z(1,0,3,1,1,3)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on sextuples of Fin 4 indices are compared. The numerator m2Num folds a fixed coupling list, summing a contribution at each term for the six indices. The companion explicitZ is a sparse case table of small integers (entries such as 4, -2, and so on) that packages the closed-form kernel.
The local module is chunk 4 of a 256-way split of the identity m2Num = 8 · explicitZ. Each chunk theorem pins one concrete sextuple so the global assembly can exhaust Fin 4^6 by case split. Upstream, both m2Num and explicitZ are pure definitions in the kernel certificate module; no analytic hypothesis is required beyond the tabulated couplings.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the integer equality for the fixed indices (1,0,3,1,1,3) and confirms they match. No lemmas are invoked beyond the evaluable definitions of m2Num (list fold of contributions) and explicitZ (pattern match on the sextuple).
why it matters
This cell feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every Fin 4 sextuple and discharges the goal by exhaustive fin_cases. That global equality is the algebraic core of the Regge exact midpoint M2–TT identity in 4D: the folded numerator is exactly eight times the explicit kernel, so curvature and stress-energy bookkeeping stay integer-exact on the lattice.
Within Recognition Science gravity work, such kernel identities underwrite discrete curvature matching before continuum limits or phenomenological fits. The chunking (256 decide goals) is pure scaffolding hygiene; once assembled, the identity is a single proved statement with no sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.