e_013321
plain-language theorem explainer
Pointwise identity: the midpoint mass-squared numerator at multi-index (0,1,3,3,2,1) equals eight times the explicit Z-coupling table entry there. Gravity analysts cite it when assembling the global m2Num = 8·explicitZ certificate over Fin 4^6. Proof is a single kernel decide on two concrete integers.
Claim. At the multi-index $(a,b,c,d,i,j)=(0,1,3,3,2,1)$ one has $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8\,Z_{\mathrm{expl}}(a,b,c,d,i,j)$, where $m_2^{\mathrm{num}}$ is the folded coupling contribution sum and $Z_{\mathrm{expl}}$ is the explicit integer coupling table on $(\mathrm{Fin}\,4)^6$.
background
This module is chunk 1 of a 256-way split of kernel decides establishing $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on every 6-tuple of $\mathrm{Fin},4$ indices. The setting is the 4D Regge exact-midpoint transverse-traceless identity used in the gravity analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at those indices. The explicit table $Z_{\mathrm{expl}}$ is a pattern-matched integer function on the same six indices (sample clauses send $(0,0,1,1,2,2)$ and $(0,0,1,1,3,3)$ to $4$, and several off-diagonal patterns to $-2$).
Both objects live in the kernel certificate module imported here; the chunk theorems only evaluate them at fixed concrete indices.
proof idea
One-line proof: decide. Both sides reduce to closed integer expressions (a finite fold versus a table lookup), so the kernel compares two Int literals and closes the equality. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ in the assemble module, which states $\forall(a,b,c,d,i,j:\mathrm{Fin},4),,m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and discharges the quantifiers by nested fin_cases, each leaf hitting one of these chunk decides.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint TT mass-squared numerator in 4D Regge calculus: the folded coupling sum must match eight times the closed-form Z table before higher curvature or continuum limits are trusted. It does not itself touch the forcing chain (T0–T8), RCL, or $\varphi$-ladder mass formula; it is pure discrete-gravity algebra supporting those later layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.