e_133201
plain-language theorem explainer
For the six Fin-4 indices (1,3,3,2,0,1), the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite this as one cell of the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the midpoint numerator satisfies $m_2^{\mathrm{num}}(1,3,3,2,0,1)=8\,Z_{\mathrm{expl}}(1,3,3,2,0,1)$, where $m_2^{\mathrm{num}}$ is the fold of coupling contributions and $Z_{\mathrm{expl}}$ is the closed-form integer kernel.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those indices. The comparison target $Z_{\mathrm{expl}}$ is an explicit case-table of small integers (entries such as $4$, $-2$, and so on) on the same six-index domain.
This module is chunk 7 of a partitioned kernel: the global claim is $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ at every multi-index. Each chunk discharges a block of concrete instances by decision procedure rather than by a single symbolic identity.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(1,3,3,2,0,1)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of $m_2^{\mathrm{num}}$ (fold of contributions) and $Z_{\mathrm{expl}}$ (pattern match on the six indices).
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every multi-index instance by nested fin_cases and needs each cell proved. This declaration supplies the cell for $(1,3,3,2,0,1)$. In the gravity stack it is bookkeeping for the exact midpoint M2/TT identity in 4D Regge calculus: once every cell matches, the folded numerator is identically eight times the explicit kernel, which is the algebraic content the larger identity relies on. It does not itself touch the T0–T8 forcing chain; it is local certified arithmetic inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.