e_221002
plain-language theorem explainer
For the six-index slot (2,2,1,0,0,2) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a{=}2,b{=}2,c{=}1,d{=}0,i{=}0,j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the Regge midpoint M2TT identity work, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each tuple. The comparison target is an explicit piecewise integer table $Z$ (explicitZ), whose nonzero entries are small constants such as $\pm 2,\pm 4$.
The module is chunk 10 of a 256-case decide grid: each theorem pins one concrete six-tuple. The local claim is the scalar identity $m_2^{\mathrm{num}}=8Z$ at that tuple, not a structural derivation of either kernel.
Upstream, both sides are pure definitions from the kernel certificate module; no analytic lemma is required beyond evaluating the fold and the table.
proof idea
One-line decide proof. Lean reduces both sides to concrete integers: the left-hand fold of coupling contributions at $(2,2,1,0,0,2)$, and the right-hand lookup $8\cdot Z(2,2,1,0,0,2)$, then checks equality by computation. No lemmas are invoked beyond kernel evaluation.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases over the six indices. Each chunk theorem such as this one discharges one leaf of that case split.
In the gravity analysis stack this identity certifies that the folded midpoint numerator is exactly eight copies of the explicit Regge kernel table, a bookkeeping step toward the exact 4D midpoint M2TT identity. It is computational scaffolding inside the Gravity domain, not a forcing-chain (T0–T8) landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.