e_021300
plain-language theorem explainer
Certificate that the Regge midpoint coupling numerator at index sextuple (0,2,1,3,0,0) equals eight times the tabulated explicit kernel integer at those indices. Gravity analysts assembling the global 4D midpoint M2 identity cite this as one of 256 finite-case checks. The proof is a single kernel decision on concrete integer equality.
Claim. At the index sextuple $(a,b,c,d,i,j)=(0,2,1,3,0,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(0,2,1,3,0,0)=8\,Z(0,2,1,3,0,0)$.
background
In the 4D Regge exact-midpoint analysis, two integer maps on $(\mathrm{Fin},4)^6$ are compared pointwise. The numerator $m_2^{\mathrm{num}}$ is a fold of a fixed coupling list: starting from zero, each term adds an integer contribution that depends on the six indices. The companion map $Z$ is an explicit piecewise table of small integers (values such as $4$ and $-2$ on selected patterns) intended as the closed form of that fold, up to a universal factor of eight.
This module is chunk 2 of the 256 kernel decides that discharge $m_2^{\mathrm{num}}=8Z$ on every sextuple. The local setting is pure finite enumeration over $\mathrm{Fin},4$; no continuum limit or curvature hypothesis enters.
proof idea
Both sides are closed integer expressions once the six $\mathrm{Fin},4$ arguments are fixed. The tactic decide normalizes the fold that defines the numerator and the match that defines the explicit table, then checks equality in $\mathbb{Z}$. No intermediate lemmas are invoked; the goal is a numeric identity.
why it matters
Feeds the assembled universal statement m2Num_eq_eight_explicitZ, which asserts the identity for every sextuple in $(\mathrm{Fin},4)^6$ and proves it by nested fin_cases. Each leaf is one chunk certificate; this declaration is the leaf for $(0,2,1,3,0,0)$. Together the chunks close the algebraic claim that the midpoint M2 numerator is exactly eight times the explicit kernel, a discrete step inside the 4D Regge gravity analysis. Continuum GR recovery and physical units are outside this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.