e_133302
plain-language theorem explainer
Pointwise kernel identity: the folded M2 numerator coupling at multi-index (1,3,3,3,0,2) equals eight times the explicit integer Z-kernel at that same index. Gravity analysts cite it as one of the 256 decided cases that assemble into the global m2Num = 8·explicitZ theorem. The proof is a single native decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,3,3,3,0,2)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 7 of a 256-case kernel certification that the Regge exact-midpoint M2 TT identity in 4D holds at the level of integer numerators. The ambient setting is discrete gravity on a 4-index simplex: six coordinates each run over $\mathbb{F}_4$, labeling edge and face pairings that enter the second-mass-moment coupling.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start from 0 and add each contribution term evaluated at the six indices. The comparison object $\mathrm{explicitZ}$ is a closed-form integer table on the same six indices (pattern-matched cases such as $(0,0,1,1,2,2)\mapsto 4$ and sign-flipped off-diagonal entries $\mapsto -2$). The claim under audit is one concrete cell of the asserted equality $m_2^{\mathrm{num}}=8,Z$.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are substituted into the fold definition of $m_2^{\mathrm{num}}$ and the pattern table for $Z$; Lean’s decision procedure checks integer equality. No lemmas beyond the two defining defs are invoked.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ quantifies over all six Fin 4 indices and discharges the universal statement by exhaustive fin_cases, each leaf a chunk theorem of this form. Without the pointwise cells, the global numerator identity that feeds the Regge exact-midpoint M2 TT certification would not close. In the Recognition gravity stack this is bookkeeping infrastructure for the discrete curvature/mass-moment side, not a forcing-chain landmark (T5–T8), but it is required scaffolding so later continuum or continuum-limit claims can quote a fully proved integer kernel rather than an assumed table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.