e_021010
plain-language theorem explainer
For the six-index slot (0,2,1,0,1,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the exact midpoint M2–TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(0,2,1,0,1,0)$ equals eight times the explicit integer kernel at those same indices: $N(0,2,1,0,1,0)=8\,Z(0,2,1,0,1,0)$.
background
This module is one chunk of a 256-case kernel certification that the 4D Regge midpoint numerator equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, labeling discrete directions in the 4-simplex / edge-pair bookkeeping of the midpoint scheme.
The numerator $N=\texttt{m2Num}$ is defined by folding a fixed coupling list and summing local contributions at six indices $(a,b,c,d,i,j)$. The comparison table $Z=\texttt{explicitZ}$ is a pattern-matched integer function on the same six indices (nonzero only on a thin set of pairings, e.g. values $\pm 2,4$ on selected diagonal and off-diagonal slots).
The local claim is the single point $(a,b,c,d,i,j)=(0,2,1,0,1,0)$ inside that equality $N=8Z$. Sibling theorems cover the other concrete tuples; the assemble layer quantifies over all of $\mathrm{Fin},4^6$.
proof idea
One-line decide proof. Both sides reduce to concrete integers: the left by evaluating the fold of contrib over couplingZList at the fixed indices, the right by pattern-matching explicitZ (or defaulting to zero) and multiplying by 8. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases over the six $\mathrm{Fin},4$ arguments and discharge of each point by a chunk identity of this form.
In the gravity analysis stack this closes the algebraic identity between the folded midpoint M2 numerator and the explicit TT-kernel table in 4D Regge calculus. That identity is bookkeeping infrastructure for exact discrete curvature / stress comparisons, not a derivation of continuum Einstein equations or of the RS forcing chain (T0–T8). It removes a large case-split from later analytic arguments by certifying the sparse integer table once and for all.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.