e_120100
plain-language theorem explainer
Single kernel identity: the Regge midpoint m2 numerator at multi-index (1,2,0,1,0,0) equals eight times the explicit integer Z coupling there. Gravity analysts cite it when assembling the full 4D midpoint TT identity over (Fin 4)^6. Proof is one `decide` on the concrete integer values of both sides.
Claim. For indices $(a,b,c,d,i,j)=(1,2,0,1,0,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $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 6 of a 256-case kernel certification that the midpoint Regge $m_2$ numerator equals eight times an explicit integer table $Z$ on six $\mathrm{Fin},4$ indices. The ambient setting is 4D Regge calculus analysis of the TT (transverse-traceless) sector at the exact midpoint.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each tuple $(a,b,c,d,i,j)$. The comparison object $\mathrm{explicit}Z$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern of integer values (e.g. $4$, $-2$, and zeros off the listed patterns).
The identity $m_2^{\mathrm{num}}=8,Z$ is checked pointwise; each chunk discharges a block of concrete index sextuples by kernel decision.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(1,2,0,1,0,0)$. The left side reduces by unfolding the fold over couplingZList and summing contributions; the right side multiplies the table value of $\mathrm{explicit}Z$ by eight. Equality of the resulting integers is decided in the kernel. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases on all six indices. That global identity is the certified algebraic core of the 4D Regge exact-midpoint $m_2$ TT analysis in this gravity stack.
Within Recognition Science gravity work, such kernel equalities lock discrete curvature/coupling bookkeeping before continuum or phenomenological limits are taken. This declaration is one of the 256 pointwise bricks; it does not itself touch T0–T8 or the RCL, but it hardens the discrete geometric layer those continuum claims sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.