e_023033
plain-language theorem explainer
For the six-index slot (0,2,3,0,3,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these micro-identities when assembling the exact midpoint Regge M2 TT identity in 4D. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}3$, $d{=}0$, $i{=}3$, $j{=}3$ 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
This module is chunk 2 of a 256-case kernel certification that the Regge midpoint numerator $m_2^{\mathrm{num}}$ is identically eight times a sparse explicit integer table $Z$ on $(\mathrm{Fin},4)^6$. The setting is 4D discrete gravity analysis: couplings are summed from a fixed list, and the claim is exact integer equality, not an asymptotic or continuum limit.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList and accumulating a contribution at each term. The companion table explicitZ is a pattern-matched integer function on six Fin-4 indices (typical nonzero values are $\pm 2,,4$ on a thin support). The present declaration fixes one concrete six-tuple and checks the scalar identity at that point.
proof idea
One-line decide proof. Both sides reduce to concrete Int values: the left by evaluating the fold that defines the numerator, the right by unfolding the pattern match for explicitZ at $(0,2,3,0,3,3)$ and multiplying by 8. No lemmas are invoked beyond kernel computation of closed integer expressions.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on all six indices. Each chunk lemma such as this one discharges one residual case so the global identity is a pure case split rather than a fresh algebraic derivation.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge $M_2$ TT sector in 4D: once the numerator is replaced by $8Z$, later certificates can reason on the sparse table alone. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is infrastructure under the discrete curvature/mass-side analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.