e_320321
plain-language theorem explainer
Pointwise identity: the Regge midpoint m2 numerator at multi-index (3,2,0,3,2,1) equals eight times the explicit kernel value Z at those indices. Gravity analysts cite it when assembling the full 4D m2Num = 8·explicitZ table identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,0,3,2,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel entry $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the quadratic mass-like numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each coupling triple for the six $\mathrm{Fin},4$ indices. The companion table $Z$ is an explicit integer-valued kernel on the same six indices (nonzero only on a sparse set of patterns such as $(0,0,1,1,2,2)\mapsto 4$ and sign-flipped off-diagonal pairs $\mapsto -2$).
This module is chunk 14 of the 256-case kernel certification that $m_2^{\mathrm{num}}=8Z$ holds at every multi-index. The local setting is pure finite enumeration: both sides are closed integer expressions once the indices are fixed, so each chunk is a batch of concrete equalities.
proof idea
One-line computational proof: decide evaluates both the folded numerator and $8\cdot Z$ at the concrete sextuple $(3,2,0,3,2,1)$ and checks integer equality. No algebraic lemmas are invoked beyond the definitions of the fold and the explicit kernel table.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the universal claim by fin_cases on all six indices, routing each concrete cell to its chunk theorem. Closing the full table identity is a necessary algebraic step in the exact midpoint Regge $M_2$/$TT$ analysis in four dimensions; without the pointwise matches the global factor-of-eight relation between the folded coupling numerator and the closed-form kernel cannot be certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.