e_311021
plain-language theorem explainer
For the six-index slot (3,1,1,0,2,1) on Fin 4, the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel decides. The proof is a single kernel decision (decide) on concrete integers.
Claim. For indices $a=3$, $b=1$, $c=1$, $d=0$, $i=2$, $j=1$ 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
In the 4D Regge midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling triple at the six Fin-4 indices. The companion map $Z$ is an explicit integer table on those same six indices (pattern-matched constants such as $4$, $-2$, and so on).
This module is chunk 13 of a 256-way case split that checks $m_2^{\mathrm{num}}=8Z$ pointwise. The local setting is pure integer arithmetic on a finite index set: no continuum limit and no variational argument yet, only the discrete kernel identity needed before assembly.
Upstream, $m_2^{\mathrm{num}}$ and $Z$ are the two definitions being compared; the chunk theorems supply the concrete equalities the assembler will case-split over.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed indices $(3,1,1,0,2,1)$: the left via the fold definition of $m_2^{\mathrm{num}}$, the right via $8$ times the pattern-matched $Z$ entry. Lean’s decision procedure closes the integer equality with no further lemmas.
why it matters
Feeds the parent theorem $m_2^{\mathrm{num}}=8Z$ for all Fin-4 indices, which is assembled by exhaustive fin_cases over $a,b,c,d,i,j$ and dispatches each cell to a chunk equality of this form. Without the pointwise decides, the midpoint M2TT identity kernel certificate cannot be glued together.
In the Recognition gravity stack this is bookkeeping infrastructure for the discrete Regge curvature side, not a forcing-chain landmark (T5–T8) by itself. It closes one cell of the 256-kernel grid so the global numerator identity is machine-checked rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.