e_010330
plain-language theorem explainer
Pointwise kernel identity: the summed coupling numerator at multi-index (0,1,0,3,3,0) equals eight times the explicit integer table at that point. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite it as one of 256 concrete cases. The proof is a single kernel decide on fully evaluated integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,1,0,3,3,0)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(0,1,0,3,3,0)=8\,Z_{\mathrm{expl}}(0,1,0,3,3,0)$.
background
This module is chunk 1 of a 256-case kernel certification that the 4D Regge midpoint numerator $m_2^{\mathrm{num}}$ coincides with eight times an explicit integer table $Z_{\mathrm{expl}}$. Both maps take six arguments in $\mathrm{Fin},4$ (discrete 4D simplex/edge labels) and return an integer.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it sums contribution terms contrib t a b c d i j over that list. The companion explicitZ is a pattern-matched closed form on the same six indices (sample clauses return $4$, $-2$, etc.). The local claim is the equality of these two integers at one concrete multi-index.
The ambient setting is exact algebraic certification of a midpoint M2TT identity in discrete gravity, not a continuum limit argument.
proof idea
One-line computational proof: by decide. After the six Fin 4 arguments are substituted, both sides reduce to concrete integers (the fold for the numerator and the matching clause for the explicit table). Lean’s decision procedure discharges the integer equality with no further lemmas or case splits inside this declaration.
why it matters
Parent theorem m2Num_eq_eight_explicitZ asserts the identity for every six-tuple in $(\mathrm{Fin},4)^6$. Its proof is a nested fin_cases sweep that bottoms out on chunk lemmas such as this one. Without the pointwise kernel facts, the universal assembly cannot close.
In the Recognition gravity stack this certifies that the discrete midpoint numerator is exactly eight times a sparse explicit table, a structural simplification used when matching Regge-type curvature bookkeeping to continuum limits. It is pure finite combinatorics: no continuum hypothesis, no sorry, and no link to the T0–T8 forcing chain beyond sitting in the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.