e_111101
plain-language theorem explainer
For the fixed multi-index (1,1,1,1,0,1) on Fin 4, the discrete second-moment numerator equals eight times the explicit integer kernel. Gravity analysts certifying the 4D Regge midpoint M2 TT identity cite it as one decided cell in chunk 5 of the 256-cell sweep. The proof is a single kernel decide on the resulting integer equality.
Claim. For indices $(a,b,c,d,i,j)=(1,1,1,1,0,1)$ with each entry in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit kernel value: $N_2(1,1,1,1,0,1)=8\,Z(1,1,1,1,0,1)$.
background
In the 4D Regge midpoint analysis, the second-moment numerator is obtained by folding a fixed list of coupling contributions over six indices in $\mathrm{Fin},4$. The companion object is a piecewise integer table on the same domain, recording closed-form kernel entries (values such as $4$ and $-2$ at selected multi-indices).
This module is chunk 5 of a decide sweep that checks the pointwise relation numerator $= 8\cdot$ explicit kernel across a 256-cell block. The local setting is exact discrete TT-sector identities at the midpoint configuration, not continuum Einstein gravity.
Upstream, the numerator is the fold of contrib over couplingZList, and the explicit table is the case-split integer function against which that fold is compared.
proof idea
With all six indices fixed, both sides reduce to concrete integers by unfolding the fold-definition of the numerator and the case table of the explicit kernel. The proof is the one-line tactic decide, which runs the kernel decision procedure on that integer equality and closes the goal. No intermediate lemmas or algebraic rewrites are invoked.
why it matters
This cell is consumed by the universal assembly theorem that states the numerator equals eight times the explicit kernel for every six-tuple in $\mathrm{Fin},4$, proved there by exhaustive fin_cases on the six indices. That assembly is a load-bearing step in the Regge-exact midpoint M2 TT identity certification in four dimensions, inside the gravity analysis layer of the monolith.
The chunk decomposition (here chunk 5) keeps each decide obligation small enough for the kernel while still covering the full finite domain. Completing every chunk discharges the pointwise identity that the assembly theorem packages for downstream curvature checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.