e_033013
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (0,3,3,0,1,3) equals eight times the closed-form kernel value at that same point. Gravity analysts cite it as one cell of the 256-case kernel table. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,0,1,3)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,3,3,0,1,3)=8\,Z(0,3,3,0,1,3)$.
background
In the 4D Regge exact-midpoint analysis, two integer kernels on six $\mathrm{Fin},4$ indices are compared. The folded numerator $N(a,b,c,d,i,j)$ is the sum of local contributions over a fixed coupling list. The closed form $Z$ is an explicit pattern-matched integer table on the same six indices (typical nonzero entries are $\pm 2,,4$).
This module is chunk 3 of the 256 kernel decides: it records one concrete multi-index equality $N=8Z$. The ambient claim is that the identity holds for every six-tuple in $(\mathrm{Fin},4)^6$, which is later assembled by exhaustive case split.
proof idea
Both sides evaluate to concrete integers once the six indices are fixed. The tactic decide discharges the resulting numeral equality; no algebraic rewriting or upstream lemmas are invoked beyond the definitions of the folded numerator and the explicit kernel.
why it matters
Feeds the assembly theorem that states $\forall a,b,c,d,i,j,, N=8Z$ on $(\mathrm{Fin},4)^6$. That global identity is the certified numerator half of the Regge exact-midpoint $M_2$ TT kernel comparison in 4D gravity. Without the pointwise cells, the exhaustive fin_cases assembly cannot close. It is bookkeeping inside the gravity analysis stack, not a forcing-chain (T0–T8) step, but it is required for the discrete curvature/mass-kernel identities used downstream in RS gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.