e_200010
plain-language theorem explainer
Pointwise certificate that the Regge M2 numerator at multi-index (2,0,0,0,1,0) equals eight times the explicit integer kernel Z. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ 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,0,0,1,0)$ 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 kernel value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity kernel certification. The local goal, stated in the module header, is to discharge $m_2^{\mathrm{num}}=8\cdot Z$ on a block of the $4^6=4096$ index tuples by pure decision (here chunk 8 among the 256 kernel decides).
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined as the fold of contrib over couplingZList, an integer accumulator of all coupling contributions at that multi-index. The comparison target explicitZ is a closed-form integer table on $(\mathrm{Fin},4)^6$, with sparse nonzero patterns such as $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$.
The present declaration fixes one concrete six-tuple and asserts numerical equality of the two sides.
proof idea
One-line computational proof: by decide. Lean reduces both the folded sum defining $m_2^{\mathrm{num}}$ at $(2,0,0,0,1,0)$ and the pattern-matched explicitZ value, then checks the integer equality $m_2^{\mathrm{num}}=8Z$ by the kernel decision procedure. No lemmas are invoked beyond the two definitions.
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}}=8\cdot Z$ and proves it by exhaustive fin_cases on all six indices, each case landing on a chunk theorem of this family (siblings e_200000–e_200023 and the other chunks).
In the Recognition gravity stack this identity is the certified algebraic core of the exact midpoint $M_2$ TT relation in 4D Regge calculus: the numerator built from coupling lists must match the closed kernel used downstream in curvature and mass-ladder matching. Closing every pointwise decide removes scaffolding from that identity and keeps the gravity analysis fully machine-checked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.