e_103033
plain-language theorem explainer
At multi-index (1,0,3,0,3,3), the folded Regge midpoint numerator m2Num equals eight times the explicit integer kernel Z. Gravity analysts cite this as one atomic case in the 4D midpoint M2–TT identity. The proof is a single kernel decide on concrete Fin 4 indices.
Claim. For indices $(a,b,c,d,i,j)=(1,0,3,0,3,3)$ in $\mathrm{Fin}\,4$, the midpoint 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
This module is chunk 4 of the case-by-case verification that the folded numerator equals eight times an explicit integer table on six $\mathrm{Fin},4$ indices (the 4D Regge midpoint M2–TT kernel).
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a coupling list: it sums contribution terms contrib over couplingZList at the six indices. The companion table explicitZ is a pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and other small integers on diagonal and off-diagonal patterns).
The local goal is purely algebraic bookkeeping: each concrete six-tuple is decided separately so a later assembler can reassemble the universal identity without re-running the full fold.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the closed indices $(1,0,3,0,3,3)$—the fold defining $m_2^{\mathrm{num}}$ on the left and the pattern match for $Z$ on the right—and checks integer equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$, proved by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one concrete branch of that case split.
In the Recognition gravity stack this identity is infrastructure for the exact midpoint Regge analysis in 4D: it certifies that the numerator built from couplings matches a sparse explicit kernel, scaled by eight. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is a pure discrete-tensor identity used downstream in the gravity analysis modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.