e_002020
plain-language theorem explainer
For the six-index slot (0,0,2,0,2,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these pointwise identities when assembling the global Regge midpoint M2–TT relation. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(0,0,2,0,2,0)$ equals eight times the explicit integer kernel at the same slot: $N(0,0,2,0,2,0)=8\,Z(0,0,2,0,2,0)$.
background
This module is one chunk of a 256-case kernel certification that the Regge midpoint numerator equals eight times an explicit integer table on six Fin-4 indices. The local setting is pure finite arithmetic: no continuum limit, only exact Int equalities.
The numerator $N=m2Num$ is defined by folding a fixed coupling list and summing a contribution at each tuple $(a,b,c,d,i,j)$. The comparison table $Z=explicitZ$ is a pattern-matched Int-valued function on the same six indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and several $-2$ off-diagonal slots).
The target identity is the pointwise claim $N=8Z$ at one concrete multi-index inside chunk 0. Downstream assembly will range over all $4^6$ slots by fin_cases.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left via the fold definition of m2Num over couplingZList, the right via the pattern match of explicitZ (or its default) at $(0,0,2,0,2,0)$, then the kernel checks equality of the two Int values.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m2Num,a,b,c,d,i,j=8\cdot explicitZ,a,b,c,d,i,j$ and discharges the universal claim by fin_cases into these pointwise decides.
In the Gravity analysis stack this is bookkeeping for the exact midpoint M2–TT identity in 4D Regge calculus: once every slot matches, the folded numerator is interchangeable with the closed kernel table. It does not itself invoke Recognition landmarks (phi, eight-tick, T0–T8); it is infrastructure under the discrete gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.