e_130331
plain-language theorem explainer
Single kernel point check: the midpoint Regge mass-squared numerator at Fin-4 indices (1,3,0,3,3,1) equals eight times the explicit integer coupling Z at those same indices. Gravity analysts assembling the universal m2Num = 8·Z identity over all 4^6 index tuples cite this chunk. Proof is pure computation via decide on concrete integers.
Claim. For indices $a{=}1$, $b{=}3$, $c{=}0$, $d{=}3$, $i{=}3$, $j{=}1$ in $\mathrm{Fin}\,4$, 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
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer via a local contribution map, summed from zero. The comparison target is an explicitly tabulated integer function $Z$ on the same six indices (sample values include $4$, $-2$, and other small integers on diagonal and off-diagonal patterns).
The local module is chunk 7 of a 256-way kernel split whose sole job is to discharge pointwise equalities $m_2^{\mathrm{num}}=8\cdot Z$. The ambient claim is the universal identity over all index sextuples, assembled by exhaustive case split on $\mathrm{Fin},4$.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple $(1,3,0,3,3,1)$ and checks integer equality. No lemmas beyond the definitions of the folded numerator and the explicit $Z$ table are required; both reduce to closed integer expressions at fixed indices.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and closes by fin_cases on all six indices. Each chunk theorem such as this one supplies one concrete cell of that case tree (module doc: "m2Num = 8·explicitZ, chunk 7 (256 kernel decides)").
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint mass-squared / TT-sector comparison in 4D Regge calculus. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete kernel arithmetic supporting the continuum-limit gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.