e_331001
plain-language theorem explainer
For the six-index tuple (3,3,1,0,0,1) in Fin 4, the folded numerator coupling m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2 TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=3$, $c=1$, $d=0$, $i=0$, $j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the tabulated explicit kernel entry: $\mathrm{m2Num}(3,3,1,0,0,1)=8\cdot\mathrm{explicitZ}(3,3,1,0,0,1)$.
background
In the 4D Regge midpoint analysis, the M2 TT identity is checked by comparing a folded numerator against an explicit sparse kernel. The numerator m2Num a b c d i j is the fold of contrib over couplingZList, yielding an integer for each six-tuple in $(\mathrm{Fin},4)^6$. The companion explicitZ is a pattern-matched table of small integers (entries such as $4$, $-2$, and defaults) on the same index domain.
This module is chunk 15 of the 256-cell kernel certification: each cell asserts m2Num = 8 · explicitZ at one concrete multi-index. The local setting is pure integer arithmetic on Fin 4 labels; no continuum limit or physical units enter the statement.
proof idea
One-line proof by decide. Lean reduces both sides at the fixed indices $(3,3,1,0,0,1)$ to concrete integers (via the fold definition of the numerator and the pattern match of the explicit kernel) and checks equality by the kernel decision procedure. No lemmas beyond the two definitions are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ quantifies over all six Fin 4 indices and discharges the identity by exhaustive fin_cases, each branch landing on one chunk cell such as this one. Without the per-cell decides, the assemble step cannot close. In the Recognition gravity stack this certifies the discrete midpoint M2 TT kernel identity used in the Regge-sector analysis; it is bookkeeping infrastructure rather than a forcing-chain landmark (T5–T8), but it is required for the exact algebraic identity that those continuum claims rest on when specialized to the midpoint stencil.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.