e_011200
plain-language theorem explainer
For the six-index slot (0,1,1,2,0,0) 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 M2TT 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 $(0,1,1,2,0,0)$ equals eight times the explicit integer kernel at the same slot: $N(0,1,1,2,0,0)=8\,Z(0,1,1,2,0,0)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity: the claim that the folded numerator m2Num equals eight times a sparse closed-form table explicitZ on every six-tuple of Fin-4 indices. The module doc states the local goal as "m2Num = 8·explicitZ, chunk 1 (256 kernel decides)."
m2Num a b c d i j is the integer obtained by folding a fixed coupling list, adding each term's contribution at those indices. explicitZ is a pattern-matched Int table on the same six Fin-4 arguments (nonzero only on a short list of index patterns such as (0,0,1,1,2,2)mapsto 4 and (0,0,1,2,1,2)mapsto -2).
The full identity is proved by exhaustive case split; each chunk theorem discharges one concrete six-tuple so the assembler can finish by fin_cases.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers (left via the fold definition of the numerator, right via the pattern match on the explicit table, then multiplication by 8), and the decidable equality on Int closes the goal with no lemmas beyond the two definitions.
why it matters
Feeds the universal statement m2Num_eq_eight_explicitZ in the assemble module, which asserts $\forall a,b,c,d,i,j,; N=8Z$ and proves it by six nested fin_cases that land on chunk theorems such as this one. That identity is the algebraic core of the exact midpoint M2TT certificate for 4D Regge gravity in the Recognition Science stack: it converts a summed coupling expression into a sparse closed form usable in curvature and mass-gap arguments. No T0–T8 forcing step is touched directly; the result is pure discrete-gravity bookkeeping supporting the continuum limit claims higher in the Gravity analysis tree.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.