e_020000
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (0,2,0,0,0,0) equals eight times the explicit integer table entry. Gravity analysts assembling the 4D Regge midpoint M2/TT kernel cite it as one of 256 decided cases. Proof is a single kernel `decide` on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,0,0,0)$ in $(\mathrm{Fin}\,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
This module is chunk 2 of a 256-case kernel certification that the 4D Regge exact-midpoint numerator equals eight times a closed-form integer table. The ambient setting is discrete gravity analysis: verifying an algebraic M2/TT identity by exhaustive evaluation on $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling entry at the six indices. The comparison object $\mathrm{explicitZ}$ is a pattern-matched integer table 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 local claim is only the single sextuple $(0,2,0,0,0,0)$. Sibling theorems cover the rest of the chunk; assembly glues all chunks into a universal statement.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete integers once the six indices are fixed literals, so Lean’s decision procedure discharges equality with no lemmas or rewriting. No induction or algebraic identity is invoked at this leaf.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z$ and proves it by six nested fin_cases, each leaf a chunk identity of this form. That universal equality is the certified bridge between the folded coupling definition and the explicit table used in the 4D Regge midpoint M2/TT analysis.
In the broader Recognition gravity stack this is pure discrete-kernel bookkeeping: it does not invoke the forcing chain (T5–T8), RCL, or $\varphi$-ladder mass formulae, but it hardens the algebraic substrate those continuum limits sit on. Closing all 256 decides removes a scaffolding surface from the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.