e_203233
plain-language theorem explainer
For the six-index slot (2,0,3,2,3,3) on Fin 4, the folded M2 numerator equals eight times the explicit Z kernel entry. Gravity analysts cite it as one atomic case in the 4D Regge midpoint TT identity. The proof is a single kernel decide on concrete integers.
Claim. With indices $(a,b,c,d,i,j)=(2,0,3,2,3,3)$ in $\mathrm{Fin}\,4$, the folded coupling 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
This module is chunk 8 of a case split proving $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathrm{Fin},4)^6$ for the 4D Regge exact-midpoint M2 TT identity. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer weight at the six indices, and the fold starts from zero.
The comparison target is the explicit kernel $Z:(\mathrm{Fin},4)^6\to\mathbb{Z}$, a closed pattern of small integers (entries such as $4$, $-2$, and symmetric permutations) that is meant to match the folded sum after a universal factor of eight. Upstream, both objects live in the kernel certificate module that packages the coupling list, the contribution map, and the explicit table.
Local setting: 256 decide-closed equalities per chunk, later reassembled by exhaustive fin_cases into the global identity.
proof idea
One-line kernel proof: decide evaluates both sides at the concrete six-tuple $(2,0,3,2,3,3)$. The left side runs the fold that defines the numerator; the right side looks up (or computes) $8\cdot Z$ at the same indices. No lemmas are invoked beyond decidable equality on Int.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges the quantifiers by six nested fin_cases, each leaf a chunk equality of this form. Without the pointwise matches, the assemble step cannot close.
In the gravity stack this identity is bookkeeping for the exact midpoint M2 TT kernel in 4D Regge calculus: it certifies that the summed coupling numerator is exactly eight copies of the explicit sparse kernel, so later curvature and continuum-limit arguments can quote the closed $Z$ table instead of the fold. It is pure discrete linear algebra on Fin 4 indices, not a continuum GR claim, and sits downstream of the kernel certificate definitions rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.