e_223332
plain-language theorem explainer
For the concrete index sextuple (2,2,3,3,3,2) in Fin 4, the folded Regge midpoint mass-squared numerator equals eight times the explicit integer Z-coupling. Gravity analysts cite it as one kernel cell of the 4D midpoint identity. The proof is a single decide on fully concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Write $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ for the fold of all coupling contributions at those indices, and $Z(a,b,c,d,i,j)$ for the explicit integer table of Z-couplings. Then $m_2^{\mathrm{num}}(2,2,3,3,3,2)=8\,Z(2,2,3,3,3,2)$.
background
This module sits in the 4D Regge midpoint analysis: one proves that the mass-squared numerator built by folding the coupling list equals eight times a sparse explicit integer table $Z$, index by index over $(\mathrm{Fin},4)^6$. The module doc states the local goal directly: "$m_2^{\mathrm{num}}=8\cdot\mathrm{explicit}Z$, chunk 10 (256 kernel decides)."
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of $\mathrm{contrib}$ over $\mathrm{couplingZList}$, starting from $0$. The companion table $\mathrm{explicit}Z$ is a pattern-matched $\mathrm{Int}$-valued function on six $\mathrm{Fin},4$ arguments, returning small integers such as $4$, $-2$, and so on on the nonzero support, and (implicitly) $0$ off-support. Both live in the kernel certificate module imported here.
Chunk theorems such as this one pin one sextuple at a time so the global identity can be assembled by exhaustive case split on $\mathrm{Fin},4$.
proof idea
One-line computational proof: by decide. Both sides are closed integer terms once the six indices are substituted (left via the fold definition of the numerator, right via the pattern table for $Z$), so the kernel decision procedure discharges equality with no lemmas and no manual algebra.
why it matters
The parent theorem is the full quantification m2Num_eq_eight_explicitZ: for every $a,b,c,d,i,j:\mathrm{Fin},4$, the numerator equals $8$ times explicit $Z$. That assembly runs nested fin_cases over the six indices; each concrete cell is the content of a chunk theorem like this one.
In the Recognition gravity stack this identity is bookkeeping infrastructure for the 4D Regge midpoint mass-squared kernel: it replaces a folded coupling sum by a sparse explicit table, which is what later curvature and continuum-limit arguments actually consume. It does not itself invoke the forcing chain (T5 J-uniqueness, T6 $\phi$, T7 eight-tick, T8 $D=3$), but it is part of the discrete geometric substrate those continuum claims rest on once gravity is wired in.
No open scaffold remains on this cell: the equality is decided outright.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.