e_223120
plain-language theorem explainer
At multi-index (2,2,3,1,2,0) the Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it as one of 256 concrete kernel checks assembling the global identity m2Num = 8·explicitZ. The proof is a single decide on fully evaluated integers.
Claim. For indices $a{=}2,b{=}2,c{=}3,d{=}1,i{=}2,j{=}0$ in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis the mass-squared numerator is defined by folding a fixed coupling list: each term contributes an integer depending on six $\mathbb{F}_4$ indices, and the fold starts from 0. The companion table explicitZ supplies a closed-form integer for every six-tuple (sparse nonzero pattern such as $4$, $-2$, and so on).
The module is chunk 10 of a 256-way partition of the kernel: each chunk discharges a block of concrete index tuples so that the global identity can be assembled by exhaustive fin_cases. The local claim is exactly one such tuple evaluation.
proof idea
Both sides are closed integer expressions once the six Fin 4 arguments are substituted. The tactic decide evaluates the fold that defines the numerator and the pattern-match that defines explicitZ, then checks integer equality; no lemmas beyond computational normalization are required.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the universal identity over all six Fin 4 indices and proves it by nested fin_cases, each leaf landing on a chunk equality of this form. Without the pointwise checks the assembly cannot close. In the broader gravity stack this identity certifies that the midpoint Regge M2/TT kernel matches its explicit eight-fold Z representation, a prerequisite for exact 4D curvature bookkeeping in the Recognition gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.