e_120022
plain-language theorem explainer
For the six Fin-4 indices (1,2,0,0,2,2), the folded coupling numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel cells. The proof is a single decide on the concrete integer equality.
Claim. For indices $(a,b,c,d,i,j)=(1,2,0,0,2,2)$ with each entry in $\{0,1,2,3\}$, the summed coupling numerator equals eight times the explicit kernel table entry at that multi-index: $N(1,2,0,0,2,2)=8\,Z(1,2,0,0,2,2)$.
background
This module is chunk 6 of a 256-cell kernel certification that the 4D Regge exact-midpoint numerator equals eight times a sparse explicit table. The ambient setting is discrete gravity analysis: couplings on Fin-4 index sextuples are summed into an integer numerator, then matched against a hand-written kernel.
The numerator m2Num folds a fixed coupling list, adding one integer contribution per term at the six indices. The table explicitZ is a pattern-matched Int-valued function on Fin 4^6; most patterns are zero, with a few nonzero entries such as 4 or -2 on selected diagonal and off-diagonal slots.
Chunk theorems pin one concrete sextuple each so the global assembly can discharge every case by fin_cases without re-running the fold.
proof idea
One-line computational proof: by decide. Lean evaluates both sides of the integer equality at the fixed indices (1,2,0,0,2,2) and checks they match. No lemmas are invoked beyond the definitions of the fold numerator and the explicit table.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every Fin-4 sextuple and proves it by exhaustive fin_cases on all six indices. Each chunk cell such as this one is a leaf of that case split.
In the Recognition gravity stack this closes a kernel identity used by the Regge exact-midpoint M2TT analysis in 4D: the folded coupling numerator is certified equal to eight times a sparse explicit table, so later curvature or mass-side arguments can quote the table instead of the fold. It is pure discrete bookkeeping, not a continuum GR claim, but it is required scaffolding for the 4D midpoint identity chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.