e_200111
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at index sextuple (2,0,0,1,1,1) equals eight times the explicit integer table at those same indices. Gravity analysts cite it as one of 256 kernel cells that assemble the global m2Num = 8·explicitZ statement. Proof is a single kernel decide on concrete Int values.
Claim. For indices $a{=}2,b{=}0,c{=}0,d{=}1,i{=}1,j{=}1$ in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit table entry: $m_2^{\mathrm{num}}(2,0,0,1,1,1)=8\,Z_{\mathrm{expl}}(2,0,0,1,1,1)$.
background
This module is chunk 8 of a 256-cell kernel certifying that the folded 4D Regge midpoint numerator equals eight times a closed-form integer table. Indices run over $\mathbb{F}_4$ (Lean Fin 4), labeling discrete edge/face slots in the midpoint TT identity.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: sum of local contributions contrib t a b c d i j over every term $t$ in couplingZList. The comparison target $Z_{\mathrm{expl}}$ is an explicit pattern-matched Int-valued table on six $\mathbb{F}_4$ arguments (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and several $-2$ off-diagonal slots).
Local setting (module doc): prove $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ by deciding each of the $4^6=4096$ points in chunks; this file handles one chunk of decides.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed at $(2,0,0,1,1,1)$. Lean’s kernel decision procedure evaluates the fold that defines the numerator and the pattern match that defines the explicit table, then checks integer equality. No lemmas are invoked beyond the two defining defs.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall(a,b,c,d,i,j:\mathbb{F}4),, m_2^{\mathrm{num}}=8,Z{\mathrm{expl}}$ by exhaustive fin_cases on all six indices and discharge of each cell by a chunk theorem of this form. That global identity is the algebraic core of the 4D Regge exact-midpoint M2 TT certification in the Gravity analysis stack: it replaces a folded coupling sum by a sparse explicit integer kernel, enabling exact (not approximate) midpoint curvature identities used downstream in discrete gravity comparisons. Within Recognition Science this sits in the gravity/Regge layer that supports continuum limits consistent with the forced $D=3$ spatial sector (T8) once the discrete kernel is under control. No open sorry: pure decide cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.