e_210333
plain-language theorem explainer
Kernel case identity: the Regge midpoint mass-squared numerator at multi-index (2,1,0,3,3,3) equals eight times the explicit Z-table entry. Gravity analysts assembling the global 4D M2TT midpoint identity cite each such decided cell. The proof is a single kernel `decide` on a closed integer equality.
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,3,3,3)$ 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 table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin 4 indices are compared cellwise. The numerator m2Num folds a fixed coupling list, summing a local contribution at each multi-index. The companion table explicitZ is a sparse pattern of small integers (entries such as $4$, $-2$, and defaults) meant to match that fold after a universal factor of eight.
This module is chunk 9 of the 256-decide kernel split: each declaration pins one concrete six-tuple so the assembler can recombine them without re-running the full $4^6$ case tree in one proof. The local claim is pure integer arithmetic on that fixed tuple; no continuum limit or curvature hypothesis enters here.
proof idea
One-line computational proof: decide evaluates both sides of the integer equality at the concrete indices $(2,1,0,3,3,3)$ and closes the goal. No lemmas are invoked beyond the definitions of m2Num (fold of contributions) and explicitZ (pattern-matched table).
why it matters
Feeds the universal identity m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and is proved by exhaustive fin_cases over all six indices, discharging each cell by a chunk theorem of this form. That global equality is the algebraic backbone of the Regge exact-midpoint M2TT identity in 4D gravity analysis inside the monolith. It does not itself touch the RS forcing chain (T0–T8), but it is infrastructure for the discrete gravity side that must eventually match continuum limits consistent with $D=3$ spatial dimensions and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.