e_020302
plain-language theorem explainer
Pointwise kernel identity: the folded M2 numerator coupling at multi-index (0,2,0,3,0,2) equals eight times the explicit integer Z table at that same index. Gravity analysts assembling the 4D Regge midpoint M2=8Z certificate cite it as one of the 256 concrete cells. The proof is a pure `decide` on closed integer arithmetic.
Claim. For the index sextuple $(a,b,c,d,i,j)=(0,2,0,3,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint certification that the numerator mass-squared coupling equals eight times an explicit integer kernel. The ambient setting is discrete gravity on a 4-index simplex lattice: indices run in $\mathrm{Fin},4$, and couplings are integers.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each sextuple $(a,b,c,d,i,j)$. The comparison target $\mathrm{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite case table (typical nonzero entries are $\pm 2,\pm 4$).
The module header states the local goal: prove $m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$ cell-by-cell via 256 kernel decides, of which this declaration is cell chunk-2 entry $(0,2,0,3,0,2)$.
proof idea
One-line computational proof. Both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed: the left side evaluates the fold that defines $m_2^{\mathrm{num}}$, the right side looks up $\mathrm{explicitZ}$ and multiplies by 8. Lean’s decide closes the resulting integer equality; no lemmas beyond the two defining defs are invoked.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases and discharge of each cell. Without the full bank of pointwise decides, the universal M2-numerator identity in the 4D Regge midpoint kernel certificate does not close.
In the Recognition gravity stack this is bookkeeping infrastructure rather than a forcing-chain landmark: it underwrites the exact discrete curvature/mass-squared algebra used downstream of the eight-tick and $D=3$ constraints, but it does not itself invoke $J$, $\varphi$, or the RCL. It is pure finite-check scaffolding for the certified kernel table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.