e_231002
plain-language theorem explainer
For the six-index tuple (2,3,1,0,0,2) on Fin 4, the folded Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic case of the 4D midpoint M2–TT identity. The proof is a single kernel decide on two concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator at $(2,3,1,0,0,2)$ equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(2,3,1,0,0,2)=8\,Z_{\mathrm{exp}}(2,3,1,0,0,2)$.
background
This module is chunk 11 of a case split proving $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{exp}}$ on all six-tuples in $(\mathrm{Fin},4)^6$. The setting is the exact midpoint M2–TT identity for 4D Regge calculus in the Recognition gravity stack.
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 local contribution contrib. The comparison target $Z_{\mathrm{exp}}$ is an explicit integer-valued pattern match on the same six indices (sample clauses return $4$, $-2$, etc.).
Both definitions live in the kernel certificate module. The present lemma fixes one concrete multi-index and asserts numerical equality after the factor of eight.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values (the fold of m2Num at this tuple versus eight times the matching clause of explicitZ), so the kernel discharges the equality with no further lemmas or rewriting.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{exp}}$ by exhausting Fin 4 on each slot. This chunk supplies one of the decided atoms in that cover (module doc: "256 kernel decides").
In the gravity analysis layer, the identity certifies that the folded midpoint numerator agrees with the closed-form kernel used downstream in Regge curvature and continuum-limit checks. It is bookkeeping infrastructure rather than a new physical law: once every chunk is in, the assemble theorem closes the algebraic side of the 4D M2–TT midpoint claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.