e_222010
plain-language theorem explainer
For multi-index (2,2,2,0,1,0) on Fin 4, the folded Regge midpoint mass-squared numerator equals eight times the explicit integer Z-table value. Gravity analysts cite it when assembling the full pointwise identity m2Num = 8·explicitZ over all 4^6 index tuples. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,2,2,0,1,0)$ 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 table entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 10 of a 256-way case split proving that the midpoint Regge mass-squared numerator equals eight times an explicit integer kernel on every 4D multi-index. The ambient setting is discrete gravity analysis: couplings on Fin 4 labels are summed into a numerator, then matched against a closed-form table.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and accumulating each term's contribution at the six indices. The comparison table $Z$ is an explicit pattern-matched integer function on $(\mathrm{Fin},4)^6$ (sample clauses include values such as $4$, $-2$, and so on). Both live in the kernel certificate module imported here.
The local goal is purely arithmetic: discharge one concrete six-tuple so a later assembler can recombine all cases.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are substituted: the left-hand side evaluates the fold that defines the numerator, the right-hand side multiplies the pattern-matched table entry by eight. Lean’s decision procedure checks integer equality; no lemmas beyond the two definitions are required.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):\mathrm{Fin},4$ and proves it by exhaustive fin_cases on each coordinate. Each chunk theorem such as this one supplies one residual case the assembler relies on after splitting.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge analysis in 4D: it certifies that the folded coupling numerator is a uniform multiple of the explicit kernel, so downstream curvature or mass-squared identities can quote a closed table rather than a fold. It does not itself invoke the forcing chain (T0–T8), RCL, or $\varphi$-ladder; it is infrastructure inside the discrete gravity certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.