e_313322
plain-language theorem explainer
Pointwise identity: the midpoint mass-squared numerator at multi-index (3,1,3,3,2,2) equals eight times the explicit integer kernel value there. Gravity analysts assembling the full 4D Regge midpoint M2–TT identity cite this as one of 256 kernel cells. The proof is a single kernel decision on concrete Fin-4 indices.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,3,2,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer table entry: $N(3,1,3,3,2,2)=8\,Z(3,1,3,3,2,2)$.
background
In the 4D Regge exact-midpoint analysis, two integer kernels on six Fin-4 indices are compared. The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at 0 and add each contribution $\mathrm{contrib},t,a,b,c,d,i,j$. The comparison target $Z=\mathrm{explicitZ}$ is a closed integer table on the same six indices (sample cells include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
This module is chunk 13 of the 256-cell kernel certification that $N=8Z$ holds at every multi-index. The local setting is pure finite enumeration: no continuum limit and no floating-point arithmetic, only exact Int equalities on $\mathrm{Fin},4$.
proof idea
One-line computational proof: decide evaluates both sides at the concrete indices $(3,1,3,3,2,2)$. The left side runs the fold that defines the numerator; the right side looks up the explicit table and multiplies by 8. Lean’s kernel checker discharges the resulting closed integer equality. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 case into the universal statement $\forall a,b,c,d,i,j,,N=8Z$, by nested fin_cases that ultimately hit cells such as this one. Without the pointwise certificates the assembly cannot close.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint mass-squared / TT kernel in 4D Regge calculus: it certifies that the folded coupling form matches the closed integer table used downstream. It does not itself invoke the forcing chain (T0–T8), RCL, or the phi ladder; it is a finite combinatorial lemma inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.