e_201102
plain-language theorem explainer
For the six-index slot (2,0,1,1,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity in 4D cite this as one of the 256 kernel point checks. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the coupling-fold numerator at $(a,b,c,d,i,j)=(2,0,1,1,0,2)$ equals $8$ times the explicit integer kernel $Z$ at those same indices.
background
This module is one chunk of the 4D Regge exact-midpoint M2 TT identity certification. The local goal, stated in the module header, is to verify pointwise that the folded numerator equals eight times an explicit integer table: $m_2^{\mathrm{num}}=8\cdot Z$ on all $4^6=4096$ index tuples, discharged in 256-sized decide blocks.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a contribution functional at each term. The comparison value $Z(a,b,c,d,i,j)$ is an explicit piecewise integer function on $(\mathrm{Fin},4)^6$ (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$). Both live in the kernel certificate module imported here.
The present declaration fixes one concrete six-tuple in that grid. Sibling theorems cover the other tuples in the same chunk.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left by evaluating the fold of contributions at the fixed indices, the right by looking up the matching clause of the explicit kernel (or the default zero). Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and is proved by exhaustive fin_cases over the six Fin-4 indices, each leaf citing one chunk equality of this form. That identity is part of the exact midpoint M2 TT analysis in the Gravity domain of the Recognition Science mirror: it certifies that the discrete curvature/coupling numerator matches the closed-form kernel used in the 4D Regge calculus side of the forcing chain. Without the pointwise checks, the assembly step cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.