e_020231
plain-language theorem explainer
For the single multi-index (0,2,0,2,3,1) on Fin 4, the folded coupling numerator m2Num equals eight times the explicit integer table explicitZ. Gravity analysts cite it as one of 256 kernel certificates for the 4D Regge midpoint M2 TT identity. The proof is a pure kernel decision: `by decide`.
Claim. At indices $(a,b,c,d,i,j)=(0,2,0,2,3,1)\in(\mathbb{F}_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
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add a local contribution at each coupling triple. The comparison target is an explicit case table $Z$ that returns a small integer (examples in the kernel cert include $4$, $-2$, and other fixed values) on each multi-index.
The local module is chunk 2 of a 256-way split of the kernel: each chunk theorem pins one concrete index tuple so the full identity can be assembled by exhaustive Fin cases. The ambient claim is $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathbb{F}_4)^6$.
proof idea
One-line computational certificate. Both sides are closed integer terms at a fixed six-tuple of Fin-4 values, so Lean’s decide evaluates the fold that defines the numerator and the matching clause of the explicit table and checks equality in $\mathbb{Z}$. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
This is one atomic brick in the proof that the folded M2 numerator is identically eight times the explicit $Z$ table. The parent theorem m2Num_eq_eight_explicitZ quantifies over all six Fin-4 indices and discharges the universal claim by fin_cases on each coordinate; each concrete residual goal is exactly one of these chunk equalities.
In the Recognition gravity stack, that assembled identity is the algebraic core of the 4D Regge exact-midpoint M2 TT certificate: it replaces a summed coupling expression by a sparse closed form, which is what later curvature and continuum-limit arguments consume. It does not itself touch the forcing chain (T5–T8) or the RCL; it is pure discrete-gravity bookkeeping inside the midpoint kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.