e_013122
plain-language theorem explainer
Pointwise identity: the folded Regge numerator m2Num at multi-index (0,1,3,1,2,2) equals eight times the explicit kernel value explicitZ there. Gravity analysts assembling the full 4D midpoint M2TT identity cite it as one of 256 kernel cells. The proof is a single decide on concrete integers.
Claim. For the multi-index $(0,1,3,1,2,2)\in(\mathrm{Fin}\,4)^6$, the integer numerator $m_2^{\mathrm{num}}(0,1,3,1,2,2)$ equals $8$ times the explicit kernel value $Z(0,1,3,1,2,2)$.
background
This module is chunk 1 of a 256-cell kernel certification that the folded numerator of the 4D Regge exact-midpoint M2TT identity equals eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, matching the four discrete directions of the 4-simplex edge data.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at those six indices. The companion table $Z(a,b,c,d,i,j)$ is an explicit pattern-matched integer function on the same domain (sample values include $4$, $-2$, and so on for the listed index patterns).
The local claim is the equality at one concrete sextuple. Upstream, both sides are pure definitions in the kernel-cert module; no analytic hypotheses are required beyond the integer arithmetic of those defs.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are substituted into the fold definition of the numerator and the pattern match of the explicit table, so the kernel decision procedure closes the equality with no lemmas or case splits.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases and invokes each cell theorem such as this one. That global equality is the algebraic core of the Regge exact-midpoint M2TT certification in the gravity analysis stack: it replaces a folded coupling sum by an eightfold explicit kernel, clearing the numerator side of the discrete curvature identity.
In the broader Recognition Science gravity line this is bookkeeping infrastructure rather than a forcing-chain landmark (T0–T8). It does not touch $\phi$, the eight-tick octave, or the $\alpha$ band; it only discharges one of the 256 integer cells needed so the midpoint Regge identity can be cited as fully checked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.