e_011132
plain-language theorem explainer
Pointwise kernel identity: the folded coupling numerator at multi-index (0,1,1,1,3,2) equals eight times the explicit integer table entry. Gravity analysts cite it as one cell of the 256-decide chunk that assembles the universal m2Num = 8·explicitZ identity. Proof is a single native decide on concrete Int values.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,1,1,1,3,2)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the closed-form table value: $m_2^{\mathrm{num}}(0,1,1,1,3,2)=8\,Z_{\mathrm{expl}}(0,1,1,1,3,2)$.
background
This module is chunk 1 of the 4D Regge exact-midpoint $M_2$ TT-identity certification: it discharges 256 concrete equalities of the form $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating integer contributions at the six $\mathrm{Fin},4$ indices. The companion table $Z_{\mathrm{expl}}$ is an explicit pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and so on).
The local goal is purely arithmetic: evaluate both sides at one fixed multi-index and check equality in $\mathbb{Z}$. Upstream definitions supply the fold and the table; no continuum geometry is invoked at this layer.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six indices are substituted into the fold definition of $m_2^{\mathrm{num}}$ and the pattern match of $Z_{\mathrm{expl}}$. Lean’s native decision procedure discharges the resulting Int equality with no lemmas or case splits beyond what decide performs internally.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and is proved by exhaustive fin_cases on all six indices, each leaf invoking one such kernel decide (this declaration is the leaf for $(0,1,1,1,3,2)$).
In the Recognition gravity stack, that universal identity is the algebraic certificate that the discrete Regge midpoint $M_2$ numerator matches the closed-form eight-fold table, a step toward the exact TT-sector identity in 4D. It is bookkeeping, not a new physical law, but without the full 256-cell cover the assembly theorem cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.