e_030101
plain-language theorem explainer
For the six Fin-4 indices (0,3,0,1,0,1), the folded numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts cite it as one of the 256 kernel cells that assemble the global midpoint M2–TT identity. The proof is a single decide, discharging both sides by native integer evaluation.
Claim. With $a,b,c,d,i,j\in\{0,1,2,3\}$ fixed to $(0,3,0,1,0,1)$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8$ times the explicit table value $Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
The ambient module is a chunk of the 4D Regge exact-midpoint M2–TT identity certification. The numerator m2Num is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The comparison target explicitZ is a sparse six-index integer table on Fin 4, with nonzero entries such as 4 on diagonal-like pairs and −2 on mixed pairs.
Local setting (module doc): prove m2Num = 8 · explicitZ cell-by-cell across 256 kernel decides. Chunk 3 holds one block of those cells. Indices run over the four discrete directions of the 4D lattice, matching the Regge edge/face bookkeeping used upstream in the kernel certificate.
proof idea
One-line computational proof: by decide. Lean’s decision procedure evaluates both the fold that defines m2Num 0 3 0 1 0 1 and the matching clause (or default zero) of explicitZ 0 3 0 1 0 1, then checks the integer equality against the factor 8. No lemmas are invoked beyond the two definitions.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies over all six Fin 4 arguments and proves the identity by nested fin_cases; each leaf is one of these e_* cells. This cell is the (0,3,0,1,0,1) leaf in that case tree.
In the Recognition gravity stack the identity certifies that the discrete midpoint second-moment numerator matches eight times the closed-form Z table, a necessary algebraic step toward the continuum TT projection and the Regge curvature bookkeeping that feeds higher gravity claims. It does not itself invoke the forcing chain (T5–T8) or the RCL, but it is part of the certified discrete geometry layer those continuum limits rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.