e_030220
plain-language theorem explainer
Pointwise kernel identity: the folded coupling numerator at multi-index (0,3,0,2,2,0) equals eight times the explicit integer table entry. Gravity analysts cite it as one of 256 concrete checks assembling the full 4D midpoint M2–TT numerator identity. The proof is a single kernel `decide` on both integer sides.
Claim. For indices $(a,b,c,d,i,j)=(0,3,0,2,2,0)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(0,3,0,2,2,0)=8\,Z_{\mathrm{expl}}(0,3,0,2,2,0)$.
background
This module is chunk 3 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on all sextuples in $(\mathrm{Fin},4)^6$. The setting is the exact midpoint M2–TT identity for 4D Regge calculus in the Recognition gravity analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at those indices. The companion $Z_{\mathrm{expl}}$ is an explicit integer-valued table on the same six $\mathrm{Fin},4$ arguments (pattern-matched closed form, e.g. $4$, $-2$, and related entries on the diagonal and off-diagonal blocks).
The local claim is only the single sextuple $(0,3,0,2,2,0)$; sibling theorems cover the rest of the chunk.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values (the fold for the numerator versus eight times the table lookup), so the equality is discharged by computational reflection with no lemmas or case splits inside this declaration.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases on all six indices, invoking one pointwise kernel fact per cell. That global identity is the certified numerator half of the 4D Regge exact-midpoint M2–TT relation used in the gravity analysis layer. Without each chunk cell (including this one), the assembly cannot close. Landmark link is structural (exact discrete gravity identity), not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.