e_022130
plain-language theorem explainer
Pointwise identity: the folded Regge midpoint numerator at multi-index (0,2,2,1,3,0) equals eight times the explicit integer table entry. Gravity analysts cite it as one kernel cell in the 4D m2Num = 8·explicitZ certification. The proof is a single native decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,1,3,0)\in(\mathrm{Fin}\,4)^6$, the summed coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(0,2,2,1,3,0)=8\,Z_{\mathrm{expl}}(0,2,2,1,3,0)$.
background
This module is chunk 2 of a 256-cell kernel certification that the 4D Regge exact-midpoint numerator equals eight times a closed integer table. The ambient setting is discrete gravity analysis: couplings on Fin-4 multi-indices are summed, then matched to an explicit formula.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and adding each contribution at those six indices. The comparison target $Z_{\mathrm{expl}}$ is a sparse integer table on the same domain (typical nonzero values $\pm 2,,4$ on selected patterns).
The local claim is only the single sextuple $(0,2,2,1,3,0)$. Sibling theorems cover the other cells; the assembly theorem quantifies over all of $(\mathrm{Fin},4)^6$.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values (the fold for the numerator versus the table lookup, scaled by 8), and Lean’s decision procedure checks equality. No algebraic lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ by exhaustive fin_cases on all six Fin-4 arguments. Each chunk cell such as this one discharges one concrete branch of that case split.
In the Recognition gravity stack, the identity certifies that the midpoint Regge numerator is exactly eight times a sparse integer kernel, a bookkeeping step toward closed-form 4D curvature/mass-side identities. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete-kernel algebra supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.