e_022200
plain-language theorem explainer
For the six-index slot (0,2,2,2,0,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these pointwise identities when assembling the global Regge midpoint M2TT relation. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,2,0,0)$ in $\{0,1,2,3\}^6$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $N$ (Lean m2Num) is obtained by folding a fixed coupling list and summing local contributions at each multi-index. The comparison target $Z$ (Lean explicitZ) is a sparse closed-form table of small integers (entries such as $4$, $-2$, and defaults).
The module is one chunk of a 256-way case split that certifies $N=8Z$ pointwise. The ambient claim is the exact midpoint M2TT identity in four dimensions: after all index combinations are checked, the folded numerator is identically eight times the explicit kernel.
Upstream, m2Num is the fold definition and explicitZ is the pattern-matched table; neither carries a proof, only the data the decide tactic evaluates.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values at the fixed six-tuple $(0,2,2,2,0,0)$: the left via folding couplingZList with contrib, the right via the explicitZ match table scaled by 8. No lemmas are invoked; the kernel closes the equality.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases over Fin 4. Each chunk theorem such as this one discharges one concrete cell so the global identity is a pure case tree rather than a single huge decide.
In the Recognition gravity stack this identity is bookkeeping for the Regge midpoint curvature/mass kernel in 4D: once $N=8Z$ holds everywhere, downstream curvature and continuum-limit arguments can quote the closed form $Z$ in place of the folded sum. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is a certified arithmetic step inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.