e_011222
plain-language theorem explainer
For the discrete multi-index (0,1,1,2,2,2) on Fin 4, the Regge midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact 4D midpoint M2 TT identity cite this as one of the 256 kernel point checks. The proof is a single decide on a fully concrete integer equality.
Claim. The integer-valued numerator $m_2^{\mathrm{num}}$ at indices $(0,1,1,2,2,2)$ equals eight times the explicit kernel $Z$ at the same indices: $m_2^{\mathrm{num}}(0,1,1,2,2,2)=8\,Z_{\mathrm{ex}}(0,1,1,2,2,2)$.
background
In the 4D Regge midpoint analysis, the TT-sector mass-squared numerator is assembled by folding a fixed coupling list: each term adds an integer contribution at a six-tuple of face indices in Fin 4, and m2Num is that sum. The companion table explicitZ is a pattern-matched closed form on the same six-tuples, returning small integers (4, -2, and similar).
The local module is chunk 1 of the 256-point kernel certification that m2Num equals 8 times explicitZ pointwise. That identity is the algebraic content of the exact midpoint M2 TT relation used in the gravity sector.
proof idea
Both sides become closed integer expressions once the six Fin 4 arguments are fixed to 0,1,1,2,2,2. The tactic decide evaluates the fold defining m2Num and the pattern match defining explicitZ, then checks the resulting Int equality. No intermediate lemmas are required beyond those two definitions.
why it matters
This is one atomic case in the exhaustive split that proves m2Num_eq_eight_explicitZ: the universal claim that the numerator equals eight times the explicit kernel for every six-tuple in Fin 4. That assembly theorem certifies the algebraic identity behind the Regge exact midpoint M2 TT relation in 4D. In Recognition Science gravity, such kernel identities underwrite the discrete curvature bookkeeping that supports continuum limits and the dimensional side of the forcing chain (T8). It closes one of 256 decide-cells in chunk 1; no scaffolding remains on this cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.