e_120132
plain-language theorem explainer
Pointwise identity: the M2 numerator coupling at index tuple (1,2,0,1,3,2) equals eight times the explicit 4D kernel value at those indices. Gravity analysts cite it as one cell of the finite kernel table that assembles into the global m2Num = 8·explicitZ statement. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(1,2,0,1,3,2)$ in $(\mathrm{Fin}\,4)^6$, the integer numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge exact-midpoint analysis of the M2 TT identity. The numerator coupling $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at a six-index slot in $(\mathrm{Fin},4)^6$, and the fold accumulates those contributions from zero.
The comparison object is the explicit kernel table $Z$, a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite pattern of constants (typical nonzero entries are $\pm 2,\pm 4$). The local claim of the module is the scalar relation $m_2^{\mathrm{num}}=8\cdot Z$ on the whole finite domain, discharged by chunked kernel decides rather than a closed-form algebraic argument.
Chunk 6 is one block of those decides. The six indices label discrete edge/vertex slots in the 4D midpoint stencil; no continuum limit is taken at this layer.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(1,2,0,1,3,2)$ and checks integer equality. The left side reduces by unfolding the fold-definition of $m_2^{\mathrm{num}}$ over the coupling list; the right side multiplies the looked-up explicitZ entry by eight. No lemmas beyond kernel reduction are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ by exhausting $(\mathrm{Fin},4)^6$. That global identity is the certified numerator half of the Regge exact-midpoint M2 TT relation in 4D gravity analysis inside the monolith.
In the Recognition framework this is bookkeeping infrastructure for discrete curvature/mass-squared couplings on the eight-tick, $D=3$ spatial lattice (T7–T8), not a derivation of $G$ or the $\phi$-ladder itself. It closes one cell of a finite certificate so later gravity lemmas can quote a uniform factor of eight instead of re-folding the coupling list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.