e_131002
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at multi-index (1,3,1,0,0,2) equals eight times the explicit integer Z-kernel there. Gravity analysts cite it as one cell of the 256-case kernel table for the 4D Regge midpoint M2–TT identity. The proof is a single kernel decision (`decide`).
Claim. For indices $(a,b,c,d,i,j)=(1,3,1,0,0,2)$ in $(\mathbb{F}_4)^6$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel on six $\mathbb{F}_4$ indices.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six indices in $\mathbb{F}_4$ are compared. The numerator side $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 side is an explicit piecewise integer function $Z$ on the same six indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The module is chunk 7 of a 256-cell case split: one theorem per multi-index, each asserting $m_2^{\mathrm{num}}=8Z$ at that cell. The local setting is purely discrete and computational; no continuum limit or physical units enter these lemmas.
proof idea
One-line kernel proof: decide evaluates both sides of the integer equality at the concrete Fin-4 sextuple $(1,3,1,0,0,2)$ and closes the goal. No algebraic lemmas are invoked; the definitions of $m_2^{\mathrm{num}}$ (list fold of contributions) and of explicit $Z$ (pattern match) are reduced by the decision procedure.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and is proved by exhaustive fin_cases over $(\mathbb{F}_4)^6$. Each chunk cell such as this one discharges one concrete sextuple so the global identity is a finite certified table rather than an opaque computation.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2–TT relation in 4D Regge calculus: matching the folded numerator against eight times the explicit kernel is a discrete consistency check on the coupling data. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it sits downstream as certified arithmetic support for the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.