e_022302
plain-language theorem explainer
Pointwise kernel identity: the folded coupling numerator at multi-index (0,2,2,3,0,2) equals eight times the tabulated explicit integer. Gravity analysts cite it as one cell of the 4D Regge midpoint M2/TT numerator certification. The proof is a single native decide on concrete Int arithmetic.
Claim. At the multi-index $(a,b,c,d,i,j)=(0,2,2,3,0,2)$ with each slot in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(0,2,2,3,0,2)=8\,Z_{\mathrm{expl}}(0,2,2,3,0,2)$.
background
This module is chunk 2 of a 256-cell kernel that certifies $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ on every sextuple of $\mathrm{Fin},4$ indices. The setting is the 4D Regge exact-midpoint analysis of the M2/TT identity in the gravity stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at those indices. The explicit table $Z_{\mathrm{expl}}$ is a closed Int-valued pattern on the same six $\mathrm{Fin},4$ arguments (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The universal claim is assembled downstream by exhausting all index combinations; each chunk theorem such as this one discharges one concrete cell.
proof idea
One-line kernel decision. Both sides reduce to concrete integers once the six indices are fixed: the left-hand side evaluates the fold of coupling contributions at $(0,2,2,3,0,2)$, the right-hand side looks up $8\cdot Z_{\mathrm{expl}}$ at the same point. Lean’s decide closes the resulting Int equality with no lemmas beyond the definitions of the numerator fold and the explicit table.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ for all $\mathrm{Fin},4$ sextuples, which proceeds by nested fin_cases and invokes one cell identity per combination. That universal equality is the certified numerator form used in the 4D Regge exact-midpoint M2/TT identity pipeline.
In the broader Recognition gravity analysis, locking the numerator to an explicit eightfold table removes a symbolic bottleneck before continuum or continuum-limit comparisons. This declaration is pure bookkeeping: one of 256 decides that together close the chunked kernel, not a new physical law. It does not itself invoke the forcing chain (T0–T8), RCL, or the $\varphi$-ladder; those enter only if later gravity theorems import the assembled identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.