e_311321
plain-language theorem explainer
For the six-index tuple (3,1,1,3,2,1) on Fin 4, the Regge midpoint numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts assembling the full m2Num = 8·explicitZ identity cite this as one of the 256 decided kernel cells. The proof is a single `decide` on concrete integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(3,1,1,3,2,1)$ with each index in $\{0,1,2,3\}$, the midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge exact-midpoint analysis: one proves that a summed coupling numerator coincides with eight times an explicit sparse kernel on all six-tuples of Fin 4 indices.
The numerator m2Num folds a fixed coupling list, accumulating integer contributions at each multi-index. The comparison target explicitZ is a pattern-matched integer table (nonzero only on a thin set of index patterns, with values such as $\pm 2,,4$).
The local setting is chunk 13 of a 256-cell kernel partition: each cell is an equality instance at one concrete multi-index, discharged by kernel decision rather than by a symbolic closed form.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values (left via the fold definition of the numerator, right via the pattern match on explicitZ at $(3,1,1,3,2,1)$), and the kernel checks the integer equality $L = 8R$.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple on Fin 4. That global statement is the algebraic backbone of the Regge exact-midpoint $M_2$ TT identity in 4D: once every kernel cell matches, the summed numerator is identically eight times the explicit sparse kernel.
In the Recognition gravity stack this is bookkeeping infrastructure, not a new physical law. It certifies that the discrete curvature/midpoint coupling table collapses to the claimed closed form, so later continuum or continuum-limit arguments can quote a single sparse kernel instead of a fold. No T0–T8 forcing step is discharged here; the result is pure finite combinatorial verification inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.