e_121101
plain-language theorem explainer
One of 256 discrete kernel cases: the folded M2 numerator at Fin-4 indices (1,2,1,1,0,1) equals eight times the explicit Z-table entry there. Gravity analysts cite it only as a brick in the assembled identity m2Num = 8·explicitZ on all sextuples. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,1,1,0,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of $\mathrm{Fin},4$ indices. The setting is the exact midpoint M2 TT identity in 4D Regge analysis: a discrete curvature/coupling identity certified by exhaustive evaluation rather than symbolic algebra.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at the six indices. The companion $Z$ is an explicit integer-valued table on $(\mathrm{Fin},4)^6$ (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$). Both live in the kernel-cert module imported here.
The local claim is only the single point $(1,2,1,1,0,1)$; siblings cover the rest of the chunk.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values (the fold for the numerator versus the table lookup for $Z$, scaled by 8), so the equality is a closed numeric goal discharged by the decidable instance on integers. No lemmas are invoked beyond the definitions of the two sides.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and proves it by six nested fin_cases over $\mathrm{Fin},4$. Each chunk theorem such as this one closes one leaf of that case tree.
In the gravity stack this identity is bookkeeping for the exact midpoint M2 TT coupling in 4D Regge calculus: it certifies that the folded numerator matches a sparse explicit table, so later curvature or mass-squared identities can quote the table instead of re-folding. It is infrastructure inside the Gravity domain, not a T0–T8 forcing step, but it is the kind of machine-checked discrete identity the RS gravity layer relies on before continuum limits are discussed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.