e_113203
plain-language theorem explainer
Pointwise identity: the midpoint M2 numerator at multi-index (1,1,3,2,0,3) equals eight times the explicit Z-coupling table entry there. Gravity analysts cite it when assembling the full 4D Regge midpoint TT kernel identity. The proof is a single kernel `decide` on the unfolded integer equality.
Claim. For the six indices $(a,b,c,d,i,j)=(1,1,3,2,0,3)$ in $\mathrm{Fin}\,4$, the midpoint mass-squared numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit $Z$-table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 5 of a 256-way kernel split proving $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathrm{Fin},4)^6$. The setting is the exact midpoint transverse-traceless identity for the 4D Regge mass-squared kernel in the Gravity analysis stack.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution contrib t a b c d i j. The comparison target explicitZ is a closed integer table on six $\mathrm{Fin},4$ indices (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
Both definitions live in the KernelCert module; this chunk only discharges concrete sextuples by computation.
proof idea
One-line kernel proof: by decide. Lean unfolds m2Num (the fold over couplingZList) and explicitZ at the concrete indices $1,1,3,2,0,3$, reduces both sides to closed integers, and checks equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ and is proved by exhaustive fin_cases on the six indices. Each case lands on a chunk theorem of this form.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint TT kernel: once numerator and table match everywhere, downstream Regge/curvature identities can quote a single closed form rather than the fold. It is pure discrete linear algebra on the 4D index set, not a continuum GR claim, and sits under the Gravity domain rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.