e_012010
plain-language theorem explainer
For the six-index tuple (0,1,2,0,1,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic decide-cell in the 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}2$, $d{=}0$, $i{=}1$, $j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator $N(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, two integer-valued maps on six Fin-4 indices appear. The numerator $N$ (m2Num) is the fold of a fixed coupling list: each term contributes via a local weight, and the sum is taken over that list. The companion map $Z$ (explicitZ) is a sparse closed-form table of small integers (entries such as $4$, $-2$, and defaults), encoding the same algebraic content without the fold.
The module is chunk 1 of a 256-cell decide grid that checks $N=8Z$ pointwise. The factor eight is the global normalization relating the folded sum to the explicit kernel in the M2–TT identity at the exact midpoint.
Upstream, $N$ and $Z$ are defined in the kernel certificate module; this chunk only evaluates one concrete sextuple.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed indices $(0,1,2,0,1,0)$: the left via folding the coupling list, the right via the pattern-match table for $Z$ scaled by 8. Lean’s kernel decision procedure discharges the integer equality with no lemmas or case splits beyond that single decide.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases over Fin 4. Each chunk cell such as this one is a leaf of that case tree (or an equivalent decide grid), so the universal identity is only as strong as these pointwise checks.
In the Recognition gravity stack, the identity certifies that the midpoint M2 numerator matches the explicit TT kernel normalization in four dimensions. That match is bookkeeping for the discrete curvature/edge-coupling side of the Regge analysis, not a new dynamical law. It sits downstream of the kernel certificate definitions and upstream of any theorem that quotes the assembled equality for all index sextuples.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.