e_202202
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,0,2,2,0,2) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the global m2Num = 8·explicitZ certificate over (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,0,2,2,0,2)$ with each coordinate in $\mathbb{F}_4$, 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 one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certificate. 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 triple at the six $\mathrm{Fin},4$ indices. The companion table $Z$ is an explicit case-split integer function on the same six indices (sample values include $4$, $-2$, and so on).
The local claim is the scalar equality $m_2^{\mathrm{num}}=8Z$ at one concrete multi-index. The module header states the program: prove $m_2^{\mathrm{num}}=8\cdot Z$ by 256 kernel decides, of which this is chunk entry 8. Upstream, only the two definitions (the fold and the table) are required; no analytic lemma is invoked.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are fixed at $2,0,2,2,0,2$, so the equality is a closed integer comparison discharged by the decision procedure. No rewrite, induction, or named lemma is applied.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices, invoking one chunk theorem per cell. That global identity is the algebraic core of the Regge exact-midpoint $M_2$ TT certificate in 4D gravity analysis inside the monolith. It does not itself touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder; it is pure discrete tensor bookkeeping supporting the continuum limit side of RS gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.