e_211101
plain-language theorem explainer
For the six-index tuple (2,1,1,1,0,1) on Fin 4, the Regge midpoint numerator m2Num equals eight times the explicit integer table explicitZ. Gravity analysts cite it as one atomic case of the 4D M2TT identity. The proof is a single kernel `decide` on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(2,1,1,1,0,1)$. Then the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit closed-form integer $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the exact midpoint M2TT identity in 4D Regge analysis: the claim that the summed numerator m2Num equals eight times a sparse explicit integer table explicitZ, verified by 256 kernel decides per chunk.
m2Num is defined by folding a fixed coupling list and summing a local contribution at each six-index slot. explicitZ is a pattern-matched integer table on (Fin 4)^6 (typical nonzero values 4, -2, and symmetric permutations). Both live in the kernel certificate module imported here.
The ambient goal is an exact algebraic identity for the midpoint discretisation of the second-moment / TT sector, not a continuum limit statement.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete Fin 4 literals (2,1,1,1,0,1) to integers and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in (Fin 4)^6 by exhausting cases. That global equality is the certified algebraic core of the 4D Regge exact-midpoint M2TT identity used in the gravity analysis stack.
Within Recognition Science this is bookkeeping infrastructure for discrete curvature / graviton-sector identities on the eight-tick, D=3 scaffold: it does not itself force phi, alpha, or the mass ladder, but it locks a finite combinatorial identity those continuum claims rely on when the Regge midpoint calculus is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.