e_201003
plain-language theorem explainer
For the six-index slot (2,0,1,0,0,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity cite this as one of the 256 kernel decides. The proof is a single `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,0,0,3)$ 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 Regge exact-midpoint analysis for the 4D M2 TT identity, two integer-valued kernels on six Fin-4 indices are compared pointwise. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib and the fold starts at 0. The comparison target explicitZ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and defaults).
The module is chunk 8 of a 256-way case split: every concrete sextuple is discharged separately so the global identity can be reassembled by fin_cases. Local setting is purely discrete and algebraic; no continuum limit or physical units enter these decides.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed indices $(2,0,1,0,0,3)$: the left via the fold definition of $m_2^{\mathrm{num}}$, the right via the pattern table for $Z$ scaled by 8. Lean’s kernel decision procedure checks integer equality; no lemmas are invoked beyond the two definitions.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases over all six indices, each case pointing at a chunk decide such as this one. That global identity is the algebraic certificate that the midpoint M2 TT numerator matches the closed-form eightfold kernel in the Regge gravity analysis. It is bookkeeping inside the discrete 4D identity, not a continuum GR derivation, and 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.