e_313023
plain-language theorem explainer
For the single multi-index (3,1,3,0,2,3) on Fin 4, the folded M2 numerator equals eight times the closed-form explicit Z value. Gravity analysts cite it as one cell of the 256-way kernel that certifies the 4D Regge midpoint M2 TT identity. The proof is a pure kernel decide on two concrete integers.
Claim. For indices $a{=}3,\,b{=}1,\,c{=}3,\,d{=}0,\,i{=}2,\,j{=}3$ in $\mathrm{Fin}\,4$, the folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of the exhaustive certification that the 4D Regge midpoint M2 TT numerator agrees with eight times a closed-form integer kernel. The ambient setting is discrete gravity on a 4-simplex skeleton: six Fin-4 indices label pairs of edges or faces that enter the second-moment (M2) coupling.
The numerator m2Num is defined by folding a fixed coupling list and summing a local contribution at each tuple. The comparison target explicitZ is a pattern-matched integer table on the same six indices (typical entries 4, -2, and so on). The identity under check is pointwise equality of these two Int-valued maps, scaled by 8.
Upstream, both maps live in the kernel-certificate module; the present file only discharges one concrete cell of the 4^6 = 4096-point domain, grouped into decide chunks of 256.
proof idea
One-line kernel proof: by decide. Lean reduces both sides at the concrete indices (3,1,3,0,2,3) to closed integers (the fold on the left, the match on the right) and checks equality by native decision. No lemmas are invoked beyond the definitions of the two maps.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 sextuple by nested fin_cases and needs each cell proved. This declaration supplies the cell (3,1,3,0,2,3) inside chunk 13. Once all chunks land, the global identity m2Num = 8 · explicitZ is available for the Regge midpoint M2 TT analysis in 4D gravity. It is pure computational scaffolding for that algebraic identity, not a new physical law; it sits downstream of the discrete-curvature bookkeeping and upstream of any continuum or continuum-limit claims that quote the closed form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.