e_002003
plain-language theorem explainer
Pointwise kernel identity: the folded coupling numerator at multi-index (0,0,2,0,0,3) equals eight times the explicit integer table at those same indices. Gravity analysts cite it as one of 256 decide-certified cells that assemble into the global m2Num = 8·explicitZ identity. Proof is a single kernel decide on concrete Int values.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,0,2,0,0,3)$ on $\mathrm{Fin}\,4$, the summed coupling numerator equals eight times the explicit closed-form table entry: $m_2^{\mathrm{num}}(0,0,2,0,0,3)=8\,Z_{\mathrm{expl}}(0,0,2,0,0,3)$.
background
In the 4D Regge midpoint analysis, the TT-sector mass-squared numerator is built by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ accumulates integer contributions over that list. The companion table $Z_{\mathrm{expl}}$ is an explicit case-split function $\mathrm{Fin},4^6\to\mathbb{Z}$ that records the closed form expected after simplification (typical nonzero entries are $\pm 2,\pm 4$).
Module setting is chunk 0 of the 256-cell kernel: every sextuple of $\mathrm{Fin},4$ indices is certified separately by decide, then reassembled. The local claim is the single cell $(0,0,2,0,0,3)$. Upstream, both $m_2^{\mathrm{num}}$ and $Z_{\mathrm{expl}}$ are pure definitions in the kernel certificate module; no analytic hypotheses are carried.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values (left via the fold definition of $m_2^{\mathrm{num}}$, right via the case table of $Z_{\mathrm{expl}}$ and multiplication by 8), so the equality is a decidable integer comparison with no lemmas invoked.
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 over the six indices, dispatching each cell to its chunk decide (this declaration is the $(0,0,2,0,0,3)$ cell).
That global identity is the algebraic backbone of the exact midpoint M2 TT identity in 4D Regge gravity analysis: it replaces a folded sum by a sparse explicit table, enabling closed-form checks of the TT mass-squared numerator. Within Recognition Science gravity work this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8), but it is required before continuum or continuum-limit claims can quote an exact discrete numerator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.