e_202121
plain-language theorem explainer
For the six-index slot (2,0,2,1,2,1) 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 in 4D cite this as one of the 256 kernel decides. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=0$, $c=2$, $d=1$, $i=2$, $j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $N_2(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2 TT identity certification. The local goal, stated in the module header, is to prove $N_2 = 8\cdot Z$ pointwise on $\mathrm{Fin},4^6$ by splitting the $4^6 = 4096$ cases into decide-sized chunks (here chunk 8, 256 kernel decides).
The numerator $N_2$ (Lean m2Num) is the fold of a contribution function over a fixed coupling list: it accumulates integer edge/face weights for six simplex indices. The closed form $Z$ (Lean explicitZ) is a sparse pattern-matched table on those same six indices, returning small integers such as $4$, $-2$, and so on for the nonzero support.
Upstream, both $N_2$ and $Z$ are defined in the kernel certificate module; this chunk only evaluates one concrete sextuple.
proof idea
One-line kernel proof: by decide. Lean reduces both sides at the concrete Fin-4 literals $(2,0,2,1,2,1)$ to integers and checks equality by computation. No lemmas are invoked beyond the definitions of the fold numerator and the explicit table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N_2 = 8Z$ and discharges the claim by exhaustive fin_cases over all six indices, routing each sextuple to its chunk equality (this one among them).
In the gravity analysis stack this identity is the algebraic core of the exact midpoint M2 TT certificate in 4D Regge calculus: once $N_2 = 8Z$ is global, the midpoint curvature/mass-squared numerator collapses to a sparse closed form. It is bookkeeping inside the discrete gravity pipeline, not a forcing-chain (T0–T8) step, but it is required for a sorry-free 4D kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.