e_211113
plain-language theorem explainer
One of 256 kernel equalities: the Regge midpoint M2 numerator at index tuple (2,1,1,1,1,3) equals eight times the explicit Z value there. Gravity analysts cite it only as a brick in the full pointwise identity. The proof is a single `decide` on concrete integer arithmetic.
Claim. For indices $a=2$, $b=1$, $c=1$, $d=1$, $i=1$, $j=3$ in $\mathrm{Fin}\,4$, the folded M2 numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis the M2 numerator is defined by folding a fixed coupling list: each term contributes an integer depending on six $\mathrm{Fin},4$ indices, and the fold starts at zero. The companion map explicitZ is a sparse pattern-matched integer table on the same six indices (typical nonzero values $\pm 2,,4$).
The local module is chunk 9 of a 256-way case split that asserts the pointwise identity numerator $= 8\cdot Z$. The surrounding kernel-cert module supplies both definitions; no continuum geometry is invoked here, only finite integer arithmetic on the discrete index cube.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides on the concrete sextuple $(2,1,1,1,1,3)$ and checks integer equality. No lemmas are invoked beyond the reducibility of the fold that defines the numerator and the pattern match that defines explicit $Z$.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases. That global equality is the algebraic certificate that the midpoint M2 tensor contraction matches eight copies of the explicit Z kernel, a step inside the Regge-exact gravity analysis. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete bookkeeping supporting the continuum limit claims higher in the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.