e_202103
plain-language theorem explainer
For the six-index slot (2,0,2,1,0,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts assembling the 4D Regge midpoint M2 TT identity cite this as one of the 256 pointwise checks. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,\,b{=}0,\,c{=}2,\,d{=}1,\,i{=}0,\,j{=}3$ in $\mathrm{Fin}\,4$, the summed coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(2,0,2,1,0,3)=8\,Z_{\mathrm{expl}}(2,0,2,1,0,3)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator m2Num folds a fixed coupling list: it accumulates contrib(t,a,b,c,d,i,j) over every term t in couplingZList, starting from 0. The comparison target explicitZ is a pattern-matched closed form on the same six indices (sample clauses return 4, -2, and so on).
The local module is chunk 8 of a 256-way partition of the Fin-4^6 grid. Each chunk theorem asserts m2Num = 8·explicitZ at one concrete multi-index. The factor 8 is the global normalization relating the folded sum to the explicit kernel across the full identity.
Upstream, both m2Num and explicitZ live in the KernelCert module; this file only discharges one point of their equality by computation.
proof idea
One-line proof by decide. Lean reduces both sides at the concrete indices (2,0,2,1,0,3) to closed integers (the fold for m2Num and the matching clause for explicitZ) and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every a,b,c,d,i,j : Fin 4. That parent proof runs nested fin_cases over all six indices; each leaf is one of these chunk decides (here e_202103 for slot 2,0,2,1,0,3).
In the Recognition gravity stack this closes the algebraic M2 TT midpoint identity in 4D Regge calculus: the folded coupling numerator is identically eight times the explicit kernel. It is pure discrete linear algebra on Fin 4, not a continuum GR derivation, and sits downstream of the kernel certificate definitions rather than of the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.