e_021112
plain-language theorem explainer
For the concrete multi-index (0,2,1,1,1,2), the Regge midpoint numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts cite it when assembling the full pointwise identity over all Fin-4 sextuples. The proof is a single kernel decide on the two integer sides.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,1,1,2)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,2,1,1,1,2)=8\,Z(0,2,1,1,1,2)$.
background
This module is chunk 2 of a 256-case kernel certification that the Regge exact-midpoint numerator equals eight times an explicit integer table on every sextuple of directions in $\mathrm{Fin},4$.
The numerator $N=\mathrm{m2Num}$ is the fold of a fixed coupling list: each term contributes an integer weight depending on the six indices, and the fold starts at 0. The table $Z=\mathrm{explicitZ}$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (typical values $\pm 2,,4$, and sparse support).
The local claim is the single point of that identity at $(0,2,1,1,1,2)$. Sibling theorems cover the other index combinations in the same chunk.
proof idea
One-line closed proof: both sides are concrete integers once the six indices are fixed, so decide evaluates $\mathrm{m2Num},0,2,1,1,1,2$ via the fold definition and $\mathrm{explicitZ},0,2,1,1,1,2$ via the pattern match, then checks equality to $8Z$. No lemmas beyond the two definitions are required.
why it matters
Feeds the assembly theorem $\mathrm{m2Num_eq_eight_explicitZ}$, which states $\forall a,b,c,d,i,j,, N=8Z$ and discharges the universal quantifier by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each chunk theorem such as this one is a named, kernel-checked cell of that case tree.
In the gravity analysis stack this identity is the algebraic backbone of the 4D Regge exact-midpoint $M_2$/$TT$ comparison: once $N=8Z$ holds pointwise, later certificates can treat the numerator as a pure multiple of the explicit kernel rather than a fold. It is pure discrete linear algebra on $\mathrm{Fin},4$, not a continuum GR statement, and does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.