e_111132
plain-language theorem explainer
Pointwise identity: the folded M2 numerator at Fin-4 indices (1,1,1,1,3,2) equals eight times the explicit integer table at those indices. Gravity analysts cite it when assembling the full 4D Regge midpoint M2–TT kernel identity. Proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=c=d=1$, $i=3$, $j=2$ in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit table value: $N(1,1,1,1,3,2)=8\,Z(1,1,1,1,3,2)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The folded numerator $N=m2Num$ accumulates contributions by folding a fixed coupling list: each term adds a local contrib at $(a,b,c,d,i,j)$. The explicit table $Z=explicitZ$ is a sparse pattern-matched Int function on the same six indices (nonzero only on a short list of index patterns, e.g. values $4$, $-2$, etc.).
The module is chunk 5 of a 256-way kernel split: each chunk discharges a block of concrete sextuples so that the global statement $N=8Z$ can be assembled by exhaustive Fin cases. Local setting: prove $m2Num=8\cdot explicitZ$ pointwise by decide.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(1,1,1,1,3,2)$. The left side reduces by unfolding the fold over couplingZList; the right side multiplies the pattern value of explicitZ by 8. Equality of the resulting integers is discharged by the kernel decision procedure. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathbb{F}_4,; N=8Z$ by nested fin_cases over all six indices. Each chunk identity such as this one is a leaf in that exhaustion; without the pointwise facts the global kernel certificate does not close.
In the broader gravity stack this supports the exact midpoint M2–TT identity used in the 4D Regge analysis (discrete curvature / deficit bookkeeping). It is pure integer algebra on the coupling table, not a continuum GR claim, and sits downstream of the kernel certificate definitions rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.