e_011333
plain-language theorem explainer
For the six-index pattern (0,1,1,3,3,3) 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. For indices $a{=}0$, $b{=}1$, $c{=}1$, $d{=}3$, $i{=}3$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,1,1,3,3,3)=8\,Z(0,1,1,3,3,3)$.
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 $N=8Z$ pointwise on a block of the $4^6$ index space by kernel decides.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution for each table entry at the six Fin-4 indices. The closed form $Z=\mathrm{explicitZ}$ is a sparse integer table on the same six indices (typical nonzero values $\pm2,,4$).
The full identity is $\forall a,b,c,d,i,j\in\mathrm{Fin},4,; N=8Z$. Individual chunk theorems pin single tuples so the assembler can discharge the universal quantifier by exhaustive fin_cases.
proof idea
One-line proof by decide. Both sides are closed integer expressions once the six concrete Fin-4 values are substituted: the left side evaluates the fold of contributions, the right side looks up (or defaults) the explicit kernel and multiplies by 8. Lean’s kernel decision procedure checks equality of the resulting integers.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $\mathrm{Fin},4$ by nested fin_cases and invokes each chunk lemma such as this one. That universal equality is the algebraic core of the Regge exact-midpoint M2 TT identity in four dimensions: it certifies that the folded coupling numerator is exactly eight times the sparse explicit kernel, with no residual terms.
In the Recognition gravity stack this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8). It closes a finite case in the 4D discrete curvature/TT analysis so later continuum or continuum-limit arguments can quote a fully discharged integer identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.