e_202301
plain-language theorem explainer
For the six-index slot (2,0,2,3,0,1) on Fin 4, the folded coupling numerator m2Num equals eight times the closed-form integer table explicitZ. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2 TT identity. The proof is a single kernel decide on both integer sides.
Claim. For indices $(a,b,c,d,i,j)=(2,0,2,3,0,1)$ with each index in $\{0,1,2,3\}$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of a brute-force certification that the 4D Regge midpoint M2 TT numerator matches a closed form: $m_2^{\mathrm{num}}=8\cdot Z$ on every six-tuple in $(\mathrm{Fin},4)^6$.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a contribution function over a fixed coupling list couplingZList, yielding an integer for each multi-index. The companion table explicitZ is a pattern-matched integer function on the same six Fin 4 arguments (sample clauses give values such as $4$, $-2$, etc.).
The local goal is not a continuum GR identity; it is exact integer equality of two fully concrete combinatorial expressions arising in the discrete curvature bookkeeping.
proof idea
One-line proof: by decide. Both sides are closed integer terms once the six concrete Fin 4 indices are substituted, so the kernel evaluates the fold that defines $m_2^{\mathrm{num}}$ and the pattern match that defines $Z$, then checks equality. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ by nested fin_cases on all six indices; each leaf is one of these chunk theorems. Without the per-slot equalities, the assemble proof has nothing to discharge.
In the Recognition gravity stack this is pure discrete bookkeeping support for the Regge midpoint M2 TT identity in 4D, not a forcing-chain (T0–T8) step. It closes one of the 256 decide obligations in chunk 8 so the global numerator identity can be cited as proved rather than scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.