e_201313
plain-language theorem explainer
At index tuple (2,0,1,3,1,3), the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these pointwise decides when assembling the global 4D midpoint Regge identity. The proof is a single kernel decide on concrete integers.
Claim. For the six $4$-valued indices $(a,b,c,d,i,j)=(2,0,1,3,1,3)$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
This module is one chunk of the 256-point kernel certification that the 4D midpoint Regge numerator equals eight times a sparse explicit table. The ambient setting is discrete gravity analysis: couplings on a 4-index lattice are summed into an integer numerator, then matched against a hand-written closed form.
The numerator m2Num is defined by folding a contribution function over a fixed coupling list: it accumulates every term that can touch the six free indices in Fin 4. The comparison target explicitZ is a sparse pattern-matched integer table on the same six indices (typical nonzero entries are $\pm 2$ or $4$).
Chunk 8 isolates a block of those index sextuples and discharges each equality by kernel decision rather than by symbolic algebra.
proof idea
One-line proof by decide. Both sides evaluate to concrete integers once the six Fin 4 arguments are fixed to $2,0,1,3,1,3$: the left side runs the fold that defines the numerator, the right side looks up (or defaults) the explicit table and multiplies by eight. Lean’s kernel checker confirms the two integers coincide.
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 invokes each pointwise chunk lemma such as this one. That global equality is the algebraic backbone of the exact midpoint $M_2$ TT identity in 4D Regge analysis inside the Gravity domain of the monolith.
In the broader Recognition framework this sits downstream of the forcing chain’s $D=3$ spatial conclusion and the discrete octave structure: the 4-index combinatorics are the lattice shadow of the continuum identity being certified. Closing all 256 decides removes scaffolding from the numerator–kernel match and lets later curvature or continuum-limit arguments quote a fully proved algebraic identity rather than a numerical spot check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.