e_212331
plain-language theorem explainer
Pointwise integer identity: the folded numerator coupling at multi-index (2,1,2,3,3,1) equals eight times the explicit kernel value at that same index. Gravity analysts cite it as one cell of the 4D Regge midpoint M2–TT kernel table. The proof is a pure `decide` on both integer sides.
Claim. For indices $a{=}2,\,b{=}1,\,c{=}2,\,d{=}3,\,i{=}3,\,j{=}1$ in $\mathrm{Fin}\,4$, the folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, the numerator coupling $m_2^{\mathrm{num}}$ is defined by folding a fixed contribution list over six $\mathrm{Fin},4$ indices: each term adds an integer contrib and the fold starts at zero. The companion explicitZ is a closed pattern-match table on the same six indices, returning small integers such as $4$, $-2$, and so on for the nonzero kernel cells.
The local module is chunk 9 of a kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ holds at every multi-index. The full quantified statement is assembled downstream by exhaustive fin_cases; each chunk supplies a block of pointwise equalities so the kernel stays decidable in pieces.
proof idea
One-line computational proof: decide evaluates both sides as concrete Int values (the fold for $m_2^{\mathrm{num}}$ at $(2,1,2,3,3,1)$ and eight times the matched explicitZ clause) and closes the equality in the kernel. No lemmas beyond the two definitions are invoked.
why it matters
This cell is consumed by m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by six nested fin_cases over $\mathrm{Fin},4$. Without the pointwise decides, the assembly theorem has nothing to discharge at this index.
In the broader gravity stack the identity certifies that the folded Regge midpoint numerator matches the explicit eightfold kernel used in the 4D M2–TT analysis. It is bookkeeping rather than a new physical law, but it is load-bearing for any later claim that quotes the closed-form $Z$ in place of the fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.