e_321210
plain-language theorem explainer
Pointwise check that the Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z at multi-index (3,2,1,2,1,0). One of 256 kernel decides in chunk 14; the assembly theorem cites it when packaging the full identity. Proof is a single native decide on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,1,2,1,0)$ with each entry 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 kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a coupling list: sum of local contributions over that list. The explicit kernel $Z$ is a closed-form case table on the same six indices (sample values include $\pm 2,4$).
The module is chunk 14 of a 256-case kernel certification: each concrete sextuple is checked separately so the global identity can be assembled by exhaustive fin_cases. Local setting is purely algebraic (no continuum limit yet): verify $m_2^{\mathrm{num}}=8Z$ pointwise on the discrete index cube.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(3,2,1,2,1,0)$. Left side runs the fold definition of $m_2^{\mathrm{num}}$; right side looks up $8\cdot Z$ from the explicit case table. Equality of the resulting integers is decided by the kernel with no manual case split.
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}}=8Z$ and discharges the claim by fin_cases over all six Fin-4 indices, invoking each chunk decide (including this one). That global identity is the algebraic core of the Regge exact midpoint $M_2$–TT relation in 4D within the Gravity analysis stack. It does not itself touch T0–T8 or the phi ladder; it is discrete kernel bookkeeping that later continuum or curvature statements rely on being exact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.