e_012131
plain-language theorem explainer
For the six Fin-4 indices (0,1,2,1,3,1), the folded numerator coupling m2Num equals eight times the explicit integer table explicitZ. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2–TT kernel identity. The proof is a single kernel decide on concrete integers.
Claim. With indices $(a,b,c,d,i,j)=(0,1,2,1,3,1)$ in $\mathrm{Fin}\,4$, the folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer via a local contribution function, summed from zero. The companion map $Z$ is an explicit case table on the same six indices (sample values include $4$, $-2$, and so on).
The module certifies the pointwise identity $m_2^{\mathrm{num}}=8Z$ by splitting the $4^6$ index space into decide-chunks. This declaration is one atom of chunk 1. Upstream, both maps live in the kernel certificate module; downstream assembly recombines the atoms by exhaustive fin_cases.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete indices $(0,1,2,1,3,1)$ to closed integers (the fold for $m_2^{\mathrm{num}}$ versus eight times the matching explicitZ clause) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the two maps.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states the universal identity $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and discharges it by six nested fin_cases, each leaf a chunk atom such as this one. Without the pointwise equals, the assemble step cannot close.
In the gravity stack this identity is bookkeeping for the exact midpoint M2–TT kernel in 4D Regge calculus: it guarantees the folded coupling numerator is exactly eight copies of the closed-form integer table, so later curvature or deficit identities can quote a single explicit $Z$ rather than a fold. It is pure discrete linear algebra on $\mathrm{Fin},4$, not a continuum GR claim, and sits well downstream of the forcing chain’s $D=3$ spatial step only as ambient dimension context for the 4D spacetime complex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.