e_101112
plain-language theorem explainer
For the six Fin-4 indices (1,0,1,1,1,2), the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over the 4D Regge midpoint kernel. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=1,b=0,c=1,d=1,i=1,j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start from $0$ and add a contribution term for each coupling triple at the six index slots. The companion map $\mathrm{explicitZ}$ is a pure pattern-match table $\mathrm{Fin},4^6\to\mathbb{Z}$ that records the closed-form integer the fold is expected to hit (typical values $\pm 2,\pm 4$, and zeros off the listed patterns).
This module is chunk 4 of a 256-way kernel split: each theorem pins one concrete six-tuple so the assembler can recombine them by exhaustive fin_cases. The local claim is exactly the instance $(1,0,1,1,1,2)$.
proof idea
One-line decide. Both sides reduce to concrete Int values: the left by evaluating the fold of contrib over couplingZList at the fixed indices, the right by looking up explicitZ 1 0 1 1 1 2 and multiplying by 8. No lemmas beyond kernel computation are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z$ by casing on all six indices and dispatching each cell to a chunk identity of this form. That global equality is the algebraic certificate that the midpoint TT mass-squared numerator in the 4D Regge kernel collapses to an explicit sparse integer table, a prerequisite step in the gravity-side exact-identity chain. It does not itself touch T0–T8 or the RCL; it is pure discrete kernel bookkeeping inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.