e_330232
plain-language theorem explainer
For the Fin-4 multi-index (3,3,0,2,3,2), the folded TT coupling numerator equals eight times the closed-form kernel integer. Gravity analysts certifying the 4D Regge exact-midpoint M2 TT identity cite this as one kernel cell in chunk 15. The proof is a single native decide on concrete integer arithmetic.
Claim. For indices $a=3$, $b=3$, $c=0$, $d=2$, $i=3$, $j=2$ in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(3,3,0,2,3,2)=8\,Z_{\mathrm{expl}}(3,3,0,2,3,2)$.
background
In the 4D Regge exact-midpoint analysis, the TT-sector mass-squared numerator is a six-index integer obtained by folding a fixed coupling list. Concretely, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums the contribution of each table entry over that list. The companion map $Z_{\mathrm{expl}}$ is a sparse pattern on $(\mathrm{Fin},4)^6$ with small integer values (e.g. $4$, $-2$) on selected multi-indices and zero elsewhere.
This module is chunk 15 of the kernel certification that $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ pointwise ("256 kernel decides"). Upstream, both sides are pure definitions: the fold for the numerator and the pattern-match table for the explicit kernel. The local goal is only the single cell with indices $(3,3,0,2,3,2)$.
proof idea
One-line computational proof: by decide. Both sides are closed integer terms once the six Fin-4 arguments are concrete, so the decision procedure evaluates the fold that defines the numerator and the pattern match that defines the explicit kernel, then checks equality. No intermediate lemmas are invoked beyond those two definitions.
why it matters
The cell is consumed by the universal assembly theorem $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ for all six Fin-4 indices, proved by exhaustive fin_cases. That assembly is the certified bridge from the folded coupling definition to the closed-form kernel in the Regge exact-midpoint M2 TT identity in 4D. Inside Recognition Science gravity work, the identity is bookkeeping for discrete curvature that must stay consistent with the broader forcing chain (including $D=3$ and the eight-tick octave); this declaration itself is pure kernel arithmetic, not a continuum or observational claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.