e_011233
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (0,1,1,2,3,3) equals eight times the explicit kernel entry there. Gravity analysts assembling the 4D Regge midpoint M2 TT identity cite it as one kernel cell. Proof is a single native `decide` on concrete integers after unfolding the fold and the explicit table.
Claim. For the multi-index $(0,1,1,2,3,3)\in(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(0,1,1,2,3,3)=8\,Z_{\mathrm{expl}}(0,1,1,2,3,3)$.
background
This module is chunk 1 of a 256-cell kernel certification that the folded numerator m2Num equals eight times the closed-form table explicitZ on every 6-tuple of indices in $\mathbb{F}_4$. The ambient setting is the exact midpoint analysis of the 4D Regge M2 TT identity in the Gravity.Analysis stack.
m2Num a b c d i j is defined by folding contrib over couplingZList and summing into an Int. explicitZ is the sparse explicit integer table on the same six Fin 4 arguments (nonzero only on a short list of index patterns, e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$). The claim here is the single cell at $(0,1,1,2,3,3)$.
proof idea
One-line computational proof: by decide. Lean unfolds the fold that defines the numerator and the match that defines the explicit table at the six concrete Fin 4 values, reduces both sides to closed integers, and checks equality by the decision procedure. No lemmas are invoked beyond the two defining defs.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j)\in(\mathbb{F}_4)^6$ and discharges the universal claim by exhaustive fin_cases on the six indices. Each cell such as this one is a certified kernel entry in that case split. In the broader RS gravity stack this is bookkeeping for the exact discrete midpoint form of the 4D Regge M2 TT identity, not a continuum or phenomenological claim. It does not itself touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.