e_210102
plain-language theorem explainer
For the six-index slot (2,1,0,1,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 exhaustive kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,b{=}1,c{=}0,d{=}1,i{=}0,j{=}2$ in $\mathrm{Fin}\,4$, 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
This module is chunk 9 of the exhaustive 256-cell certification that the Regge midpoint M2TT numerator equals eight times a closed-form integer kernel on four-dimensional index data. Indices run over $\mathrm{Fin},4$, matching the 4D simplex/edge labeling used in the surrounding gravity analysis.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on six $\mathrm{Fin},4$ arguments (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local claim is the single cell with arguments $(2,1,0,1,0,2)$. Sibling theorems cover the other cells in the same chunk; the assemble theorem quantifies over all six indices.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides at the concrete Fin 4 sextuple $(2,1,0,1,0,2)$: the fold defining $m_2^{\mathrm{num}}$ reduces to an integer, $\mathrm{explicitZ}$ matches its table clause (or default), and equality of the resulting integers is discharged by the decidable instance on $\mathrm{Int}$. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every cell by nested fin_cases on $a,b,c,d,i,j$ and dispatches each branch to a chunk theorem of this form. Without the cell equalities, the universal identity $m_2^{\mathrm{num}}=8,Z$ on $\mathrm{Fin},4^6$ does not close.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge M2TT kernel in 4D: it converts a summed coupling expression into an explicit sparse integer table, which later analysis can quote without re-folding. It is computational certification inside the gravity analysis layer, not a forcing-chain (T0–T8) step, but it underwrites exact discrete curvature identities used downstream of the continuum RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.