e_220113
plain-language theorem explainer
One of 256 kernel equalities asserting that the midpoint Regge m2 numerator at multi-index (2,2,0,1,1,3) equals eight times the explicit closed-form Z value at those indices. Gravity analysts assembling the 4D midpoint M2TT identity cite it as a single finitary case. The proof is a pure `decide` on integer arithmetic.
Claim. For the six indices $(a,b,c,d,i,j)=(2,2,0,1,1,3)$ in $\{0,1,2,3\}$, 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 quadratic mass-like numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at six Fin 4 indices, and the fold starts from zero. The companion explicitZ is a sparse pattern-matched integer table on the same six indices (typical nonzero values $\pm 2,\pm 4$).
The local module is chunk 10 of a 256-case kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The ambient goal is an exact algebraic identity for the midpoint M2TT operator in four dimensions, reduced to finitely many integer checks because every index runs over a four-element type.
proof idea
One-line kernel discharge: by decide. Lean evaluates both sides as concrete Int expressions (the fold of m2Num at the fixed indices versus 8 * explicitZ at those indices) and closes the equality by computational reflection. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by exhaustive fin_cases on all six indices, each case landing on a chunk theorem such as this one. That global identity is the certified numerator half of the Regge exact midpoint M2TT 4D kernel. Within Recognition gravity, it is bookkeeping infrastructure for the discrete curvature/mass ladder rather than a forcing-chain landmark (T5–T8); it closes one of the 256 finitary obligations so the midpoint identity can be cited without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.