e_320223
plain-language theorem explainer
For the six-index tuple (3,2,0,2,2,3) on Fin 4, the folded coupling numerator m2Num equals eight times the closed-form explicitZ value. Gravity analysts cite it as one of the 256 kernel cells that assemble the global m2Num = 8·explicitZ identity. The proof is a single decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the coupling-fold numerator at $(a,b,c,d,i,j)=(3,2,0,2,2,3)$ satisfies $m_2(3,2,0,2,2,3)=8\,Z_{\mathrm{expl}}(3,2,0,2,2,3)$.
background
In the 4D Regge midpoint analysis, m2Num(a,b,c,d,i,j) is the integer obtained by folding the coupling list and summing each contribution at those six Fin-4 indices. explicitZ is the sparse closed form that returns a small integer (typically 4, -2, or 0) on the support of the kernel and zero elsewhere.
The module is chunk 14 of the 256-cell decide grid that checks m2Num = 8·explicitZ pointwise. The local setting is pure integer arithmetic on Fin 4; no continuum limit or physical units enter the statement.
Upstream, both m2Num and explicitZ are defined in the kernel certificate module; the present cell only evaluates them at one concrete multi-index.
proof idea
One-line kernel proof: by decide. Lean reduces both sides to concrete Int values (the fold for m2Num and the pattern match for explicitZ) and checks equality by computation. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in Fin 4 by exhaustive fin_cases and dispatches each cell to a chunk theorem of this form. That global equality is the algebraic backbone of the Regge exact midpoint M2 TT identity in 4D: once the numerator is identically eight times the explicit kernel, the continuum TT structure follows by scaling. Within Recognition gravity this is bookkeeping infrastructure, not a forcing-chain step (T0–T8), but it closes a finite certificate that the discrete curvature coupling matches the predicted Z pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.