e_333333
plain-language theorem explainer
At the single index sextuple (3,3,3,3,3,3) in (Fin 4)^6, the folded Regge midpoint coupling numerator equals eight times the explicit integer Z table. Gravity analysts assembling the 4D midpoint M2 TT identity cite this as one of the 256 kernel cases. The proof is a pure `decide` on concrete integers.
Claim. For indices $a=b=c=d=i=j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(3,3,3,3,3,3)$ equals $8$ times the explicit integer coupling $Z(3,3,3,3,3,3)$.
background
This module is chunk 15 of the 256 kernel decides that discharge the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of $\mathrm{Fin},4$ indices. The setting is the exact midpoint analysis of the 4D Regge M2 TT identity in the Gravity.Analysis layer.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums a contribution functional over that list at the six indices. The right-hand side is the explicit integer table $Z:\mathrm{Fin},4^6\to\mathbb{Z}$, a pattern-matched lookup of small integers (entries such as $4$, $-2$, and so on).
Upstream, both $m_2^{\mathrm{num}}$ and $Z$ live in the kernel certificate module; this chunk only evaluates them at one concrete point.
proof idea
One-line computational proof: decide reduces both sides at the concrete sextuple $(3,3,3,3,3,3)$ to closed integer expressions and checks equality in $\mathbb{Z}$. No lemmas are invoked beyond the definitions of the fold and the $Z$ table.
why it matters
The parent theorem is the universal assembly m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ and proves it by exhaustive fin_cases on all six indices. Each case lands on a chunk theorem of this form; this declaration closes the all-threes corner.
In the broader Recognition gravity stack, the identity certifies that the midpoint Regge numerator factors cleanly through the explicit coupling table, a bookkeeping step toward exact discrete curvature identities in 4D. It does not itself touch the forcing chain (T0–T8) or the J-cost, but it is part of the discrete-geometry substrate those continuum limits rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.