e_322103
plain-language theorem explainer
One kernel cell of the 4D Regge midpoint identity: the integer numerator m2Num at indices (3,2,2,1,0,3) equals eight times the closed-form table explicitZ at the same point. Gravity analysts cite it when discharging the finite case split that proves m2Num = 8·explicitZ everywhere on Fin 4^6. The proof is a single kernel decide on that sextuple.
Claim. For the index sextuple $(a,b,c,d,i,j)=(3,2,2,1,0,3)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the given indices. The companion table explicitZ is a sparse pattern-matched function returning small integers (e.g. $\pm 2,,4$) on selected index patterns and (implicitly) the default elsewhere.
The local module is chunk 14 of a 256-cell decide kernel whose sole job is to check $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The ambient claim is the exact midpoint M2 TT identity in four dimensions, reduced to this finite arithmetic check on the discrete index cube.
proof idea
One-line kernel proof: decide evaluates both sides at the concrete sextuple $(3,2,2,1,0,3)$ and confirms integer equality. No lemmas are invoked beyond the definitions of m2Num (the fold over couplingZList) and explicitZ (the pattern table).
why it matters
This cell is one of the 256 decide atoms that the assembler m2Num_eq_eight_explicitZ consumes. That parent theorem states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhaustive fin_cases, so each chunk theorem closes one leaf of the case tree.
In the broader Recognition gravity stack, the equality $m_2^{\mathrm{num}}=8Z$ is the algebraic certificate that the midpoint Regge curvature contribution matches the closed-form TT kernel used downstream. It is pure discrete arithmetic support for the continuum identity, not a continuum derivation itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.