e_122002
plain-language theorem explainer
Pointwise check that the folded coupling numerator equals eight times the closed-form integer kernel at multi-index (1,2,2,0,0,2). Gravity analysts cite it as one cell of the 256-case kernel table for the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete Fin-4 data.
Claim. For indices $(a,b,c,d,i,j)=(1,2,2,0,0,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 $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer via a local contribution map, and the fold starts at $0$. The comparison target is an explicit piecewise integer function $Z$ on the same six indices (tabulated by pattern, with values such as $4$, $-2$, and so on).
This module is chunk 6 of a 256-cell decide table whose sole job is to certify $m_2^{\mathrm{num}}=8Z$ at every multi-index. The local setting is pure finite enumeration: no continuum limit and no floating-point arithmetic, only exact Int equalities on a $4^6$ grid.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(1,2,2,0,0,2)$. The left side runs the fold that defines the numerator; the right side looks up (or computes) $8Z$ at those indices. Equality of the resulting integers is discharged by the kernel decision procedure. No lemmas beyond the two defining defs are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every cell into the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$, proved by exhaustive fin_cases on the six indices. This chunk supplies the $(1,2,2,0,0,2)$ branch of that case tree.
In the broader Recognition gravity stack, the identity is a discrete algebraic certificate inside the Regge midpoint M2TT analysis in four dimensions. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it hardens a kernel step those continuum or effective-field layers may later quote when matching discrete curvature bookkeeping to continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.