e_222302
plain-language theorem explainer
Pointwise identity: the Regge midpoint numerator coupling at multi-index (2,2,2,3,0,2) equals eight times the explicit kernel value Z at those indices. Gravity analysts cite it when assembling the full 4D m2Num = 8·explicitZ certificate. Proof is a single kernel decide on concrete Fin-4 integers.
Claim. For indices $a=b=c=2$, $d=3$, $i=0$, $j=2$ in $\mathrm{Fin}\,4$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 10 of a 256-case kernel certification that the 4D Regge exact-midpoint numerator equals eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, matching discrete edge/face labels in the midpoint triangulation.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer weight at the six-index slot, and the fold sums them. The companion table $Z$ is an explicit pattern-match on those six indices, returning small integers (e.g. $4$, $-2$) on the supported patterns and (implicitly) the default elsewhere.
The local claim is only the equality at one concrete six-tuple; the surrounding chunks cover the rest of the $4^6$ grid needed for the global identity.
proof idea
One-line computational proof: decide evaluates both sides at the literal indices $(2,2,2,3,0,2)$. The left side reduces by unfolding the fold over couplingZList and summing the integer contributions; the right side multiplies the pattern-matched explicitZ entry by eight. No lemmas beyond the two definitions are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the claim by exhaustive fin_cases over $\mathrm{Fin},4$. Each chunk such as this one pins a single cell so the global certificate stays kernel-checkable rather than a monolithic tactic script.
In the gravity analysis stack this identity is bookkeeping for the Regge midpoint $M_2$ tensor structure in 4D: matching the folded numerator to an explicit sparse kernel is the algebraic step that lets later curvature or deficit identities quote a closed form instead of a sum. It does not itself invoke the RS forcing chain (T5–T8) or the J-cost; it is pure discrete-geometry arithmetic supporting the gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.