e_310002
plain-language theorem explainer
One kernel cell of the 4D Regge midpoint identity: the folded numerator m2Num at multi-index (3,1,0,0,0,2) equals eight times the explicit integer table explicitZ at the same indices. Gravity analysts assembling the global m2Num = 8·explicitZ certificate cite this cell. The proof is a single kernel decide on concrete integers.
Claim. For the six $4$-valued indices $(a,b,c,d,i,j)=(3,1,0,0,0,2)$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer value $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
The module is one chunk of the 256-cell kernel that certifies $\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ for the 4D Regge exact-midpoint $M_2$ TT identity. Indices run over $\mathrm{Fin},4$, so there are $4^6=4096$ raw cells; the assemble layer reduces the work to a structured 256-decide cover via fin_cases.
Upstream, $\mathrm{m2Num}(a,b,c,d,i,j)$ is the integer obtained by folding $\mathrm{couplingZList}$ and summing each term's contribution at those indices. $\mathrm{explicitZ}$ is the closed integer table on the same six indices (sample values include $4$, $-2$, and so on for the listed patterns). The local claim is equality of those two integers at the single multi-index $(3,1,0,0,0,2)$.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values (the fold for m2Num and the pattern match for explicitZ), so the equality is a decidable integer comparison discharged by the kernel with no lemmas or rewriting.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,;\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ and is proved by exhaustive fin_cases on the six indices, each leaf a chunk decide such as this one. 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 invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete tensor bookkeeping supporting the continuum limit story for the midpoint scheme.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.