e_121003
plain-language theorem explainer
Pointwise check that the folded Regge midpoint numerator m2Num equals eight times the explicit integer kernel table at multi-index (1,2,1,0,0,3). Gravity analysts cite it only as one of the 256 kernel decides that assemble the global identity. The proof is a single native decide on concrete integers.
Claim. At indices $(a,b,c,d,i,j)=(1,2,1,0,0,3)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel table entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on the 4D Regge-exact midpoint kernel. The ambient setting is discrete gravity analysis: integer-valued couplings on $\mathrm{Fin},4$ multi-indices that encode midpoint TT contributions.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each tuple $(a,b,c,d,i,j)$. The comparison table $Z$ is an explicit pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and so on). Both live in the kernel certificate module imported here.
The local claim is only the single evaluation at $(1,2,1,0,0,3)$; siblings cover the other tuples in the same chunk.
proof idea
One-line computational proof: decide. Lean reduces both sides at the concrete $\mathrm{Fin},4$ arguments to closed integers (the fold for $m_2^{\mathrm{num}}$ versus the pattern match for $Z$) and checks equality by the decision procedure. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ and $Z$.
why it matters
The parent theorem is $m_2^{\mathrm{num}}=8\cdot Z$ for all six indices, assembled by exhaustive fin_cases over $(\mathrm{Fin},4)^6$ and discharge of each leaf by a chunk decide such as this one. Without the pointwise facts, the global numerator-to-table identity does not close.
In the Recognition gravity stack this identity is bookkeeping for the Regge-exact midpoint mass-squared kernel in 4D, not a forcing-chain landmark (T5–T8) by itself. It keeps the discrete TT coupling table aligned with the folded definition so later continuum or phenomenological comparisons rest on a fully decided integer identity rather than an assumed normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.