e_012302
plain-language theorem explainer
Pointwise identity: the Regge midpoint mass-squared numerator at index sextuple (0,1,2,3,0,2) equals eight times the explicit Z-table entry there. Gravity analysts cite it as one kernel cell in the 4D midpoint M2–TT identity. The proof is a single kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,2,3,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$–TT identity certification. The local goal, stated in the module header, is to prove $m_2^{\mathrm{num}}=8\cdot Z$ on a block of kernel cells by pure decision.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: each term contributes an integer depending on the six $\mathrm{Fin},4$ indices, and the fold starts at $0$. The comparison target $Z$ is an explicit piecewise-integer table on the same six indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both objects live in the kernel certificate module imported here. The present declaration fixes one concrete sextuple and asserts numerical equality after scaling by eight.
proof idea
One-line kernel proof: decide. Both sides reduce to closed integer expressions once the six indices are literals, so the decision procedure checks $m_2^{\mathrm{num}}(0,1,2,3,0,2)=8\cdot Z(0,1,2,3,0,2)$ by evaluation. No lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every $\mathrm{Fin},4$ sextuple by nested fin_cases and dispatches each cell to a chunk equality of this form. Without the pointwise facts, the universal identity $m_2^{\mathrm{num}}=8Z$ does not close.
In the gravity analysis stack this identity is the algebraic backbone of the exact midpoint $M_2$–TT relation in four dimensions: it converts the folded coupling expansion into the closed $Z$-table used downstream in Regge curvature bookkeeping. It is pure discrete linear algebra on the 4-simplex index set, not a continuum GR derivation, and it does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.