e_122012
plain-language theorem explainer
Pointwise check that the Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z at multi-index (1,2,2,0,1,2). Gravity analysts cite it as one cell of the 256-case kernel table. The proof is a pure `decide` on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,2,0,1,2)$ 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 value $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 fixed coupling list: each term contributes via a local contrib and the sum is taken over that list. The comparison target is explicitZ, a sparse case-table of small integers (entries such as $4$, $-2$, and so on) encoding the closed-form midpoint kernel.
The module is chunk 6 of a 256-cell partition of the full $(\mathbb{F}_4)^6$ table. The local claim is the scalar identity $m_2^{\mathrm{num}}=8\cdot Z$ at one fixed multi-index. Upstream, both sides are pure definitions from the kernel certificate module; no analytic lemma is required beyond evaluating those definitions.
proof idea
One-line computational proof: decide. After substituting the six concrete Fin-4 indices, both sides reduce to closed integer expressions (a finite fold on the left, a table lookup on the right), and the kernel decides equality in $\mathbb{Z}$.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j)\in(\mathbb{F}_4)^6$ by exhausting all index cases. That global equality is the algebraic backbone of the exact midpoint $M_2$ TT identity in the 4D Regge analysis: it certifies that the folded coupling numerator is exactly eight copies of the explicit kernel, with no residual defect on any cell.
Within Recognition gravity, this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8). It closes one concrete cell of the kernel table so the assembled identity can be cited without gaps when matching discrete curvature weights to continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.