e_021022
plain-language theorem explainer
Pointwise identity: the summed coupling numerator at multi-index (0,2,1,0,2,2) equals eight times the tabulated explicit integer at that same index. Gravity analysts cite it when assembling the global m2Num = 8·explicitZ certificate over (Fin 4)^6. The proof is a single kernel decide on two concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,2,1,0,2,2)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(0,2,1,0,2,2)=8\,Z_{\mathrm{expl}}(0,2,1,0,2,2)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. 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 the six Fin-4 indices. The companion table $Z_{\mathrm{expl}}$ is an explicit pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and so on).
The local goal, stated in the module header, is to prove $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on a 256-point chunk of the kernel by pure decision. Sibling lemmas cover the other concrete multi-indices in the same chunk; the present declaration handles only $(0,2,1,0,2,2)$.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values (the left via the fold definition of the numerator, the right via the pattern match on the explicit table, scaled by 8), and the decidable equality checker discharges the goal with no further lemmas.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases on all six Fin-4 arguments, invoking one pointwise chunk lemma per cell. That global equality is the algebraic core of the Regge exact-midpoint $M_2$ TT identity in 4D gravity analysis inside the monolith. It sits in the Gravity domain rather than the T0–T8 forcing chain, but it is the kind of fully discharged integer identity the framework needs before continuum or continuum-limit claims can be trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.