e_021121
plain-language theorem explainer
Pointwise identity: the folded M2 numerator at multi-index (0,2,1,1,2,1) equals eight times the explicit Z-table entry there. Gravity analysts assembling the 4D Regge midpoint M2–TT kernel cite this as one of 256 kernel decides. Proof is a single `decide` on concrete integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,1,2,1)$ with each coordinate in $\mathbb{F}_4$, the folded numerator $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 table.
background
In the 4D Regge exact-midpoint analysis, the M2 numerator is defined by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums the local contributions of each coupling term at the six $\mathrm{Fin},4$ indices. The companion table $Z$ is an explicit pattern-matched integer function on the same six indices (nonzero only on a sparse set of index patterns).
This module is chunk 2 of a 256-way kernel certification that $m_2^{\mathrm{num}}=8Z$ holds at every multi-index. The factor 8 is the combinatorial normalization tying the folded sum to the closed-form kernel used in the TT-sector identity.
Upstream, m2Num is the fold over couplingZList; explicitZ is the sparse case table. Both live in the kernel-cert module imported here.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values at the fixed indices $(0,2,1,1,2,1)$, so the decision procedure discharges equality by evaluation. No lemmas beyond the definitions of the numerator fold and the explicit table are required.
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$ by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each chunk theorem such as this one is a leaf of that case tree (or an equivalent decide kernel).
In the gravity stack this closes the algebraic identity between the summed coupling numerator and the explicit midpoint kernel, a prerequisite for the Regge exact-midpoint M2–TT identity in 4D. It is pure discrete kernel bookkeeping, not a continuum GR claim; the RS forcing chain (T5–T8) is not directly invoked here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.