e_013003
plain-language theorem explainer
For the six-index slot (0,1,3,0,0,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity cite this as one of the 256 kernel decides. The proof is a pure kernel decision (`by decide`).
Claim. For indices $a{=}0,\,b{=}1,\,c{=}3,\,d{=}0,\,i{=}0,\,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 1 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 ambient setting is 4D discrete gravity analysis for an exact midpoint M2 TT identity.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a local contribution at each term. The companion $Z$ is an explicit pattern-matched integer on the same six indices (typical nonzero values $\pm 2,,4$ on a thin support). The claim is the pointwise equality at one concrete multi-index.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides of the integer equality at the fixed Fin-4 sextuple and closes by computational reflection. No lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and $Z$ are invoked.
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 over $(\mathrm{Fin},4)^6$. Each chunk theorem such as this one discharges one concrete cell so the global identity is a pure case split rather than a symbolic fold argument.
In the Recognition gravity stack this certifies the exact algebraic midpoint kernel used in the discrete TT sector, keeping the M2 numerator on a fully decided integer table before continuum or continuum-limit arguments. It is scaffolding for the larger Regge-exact midpoint identity, not a physical law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.