e_232002
plain-language theorem explainer
At multi-index (2,3,2,0,0,2) on (Fin 4)^6, the folded Regge coupling numerator equals eight times the explicit integer table entry. Gravity analysts cite it as one of the 256 kernel cases that assemble the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,3,2,0,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer value $Z(a,b,c,d,i,j)$.
background
This module is chunk 11 of a 256-case kernel certification that the 4D Regge midpoint $m_2$ numerator matches an explicit closed form. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The comparison target explicitZ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite pattern table (e.g. $(0,0,1,1,2,2)\mapsto 4$, several sign-flipped $-2$ entries, and so on).
The ambient setting is exact algebraic identities for Regge calculus at the midpoint in four dimensions, not continuum GR. Indices run in Fin 4, so every equality is a finite integer check. Upstream, only the two definitions of the numerator fold and the explicit table are needed; no analytic estimates enter.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete six-tuple $(2,3,2,0,0,2)$ to closed integers (the fold over the coupling list on the left, the table lookup on the right) and checks equality in the kernel. No lemmas beyond the definitions of m2Num and explicitZ are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the claim by exhaustive fin_cases on all six indices, each case a sibling decide of this form. The factor-of-eight match is the algebraic content of the Regge exact midpoint $m_2$ TT identity in 4D: once every kernel cell is certified, the numerator is interchangeable with the closed table in downstream gravity identities. It is pure finite bookkeeping inside the Gravity analysis stack, not a continuum curvature statement, and does not itself touch the T0–T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.