e_120320
plain-language theorem explainer
Single kernel point check: the folded M2 numerator at multi-index (1,2,0,3,2,0) equals eight times the explicit integer table entry. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite it as one of 256 Fin-4 cases. The proof is a pure `decide` on concrete integers after unfolding the fold and the table.
Claim. For indices $(a,b,c,d,i,j)=(1,2,0,3,2,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit closed-form integer $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each list entry for the given multi-index. The comparison target $Z$ is an explicit piecewise-constant table $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample clauses send $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local module is chunk 6 of a 256-way partition of that kernel identity: each chunk discharges a block of concrete index tuples so the global statement can be assembled by exhaustive case split. The ambient claim is $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathrm{Fin},4)^6$.
proof idea
One-line computational proof: decide. Lean unfolds $m_2^{\mathrm{num}}$ (the fold over the coupling list) and $Z$ (the explicit table) at the fixed six-tuple $(1,2,0,3,2,0)$, reduces both sides to concrete integers, and checks equality in $\mathbb{Z}$. No lemmas beyond the two kernel definitions are invoked.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all six $\mathrm{Fin},4$ indices, which proceeds by nested fin_cases and lands on these pointwise certificates. That identity is the algebraic core of the Regge exact-midpoint M2–TT comparison in the Gravity analysis stack: it certifies that the folded discrete curvature/mass-squared numerator matches a simple closed integer table up to the universal factor eight.
Within Recognition Science this sits in the discrete-gravity bookkeeping that supports continuum limits and effective Newtonian structure; it is not itself a forcing-chain (T0–T8) step, but a verified kernel identity those continuum arguments rely on. Closing all 256 chunks removes scaffolding from the midpoint M2 numerator comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.