e_203111
plain-language theorem explainer
For the six-index slot (2,0,3,1,1,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the exact midpoint M2 TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(2,0,3,1,1,1)$ equals eight times the explicit integer kernel at the same indices: $N(2,0,3,1,1,1)=8\,Z(2,0,3,1,1,1)$.
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 prove the pointwise identity numerator = 8 · explicit kernel on a block of the $4^6$ index space by kernel decides.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at those six Fin-4 indices. The explicit kernel $Z$ is a sparse integer table on the same six indices (typical nonzero values 4, -2, and symmetric permutations).
The present declaration fixes one concrete sextuple $(2,0,3,1,1,1)$ inside chunk 8 of that enumeration.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold of contributions at the fixed indices; the right-hand side multiplies the table lookup explicitZ 2 0 3 1 1 1 by 8. Lean’s kernel decision procedure checks equality of the resulting Int values. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in Fin 4 by exhaustive fin_cases and dispatches each cell to a chunk lemma of this form. That global equality is part of the certified algebraic core of the 4D Regge exact-midpoint M2 TT identity used in the gravity analysis stack.
In the Recognition Science gravity line, such exact discrete identities underwrite continuum limits and curvature bookkeeping without floating-point gaps. This chunk does not itself touch T0–T8 or the J-cost forcing chain; it is pure index algebra supporting the Regge side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.