e_310211
plain-language theorem explainer
For the six-index slot (3,1,0,2,1,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel point-checks that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=3$, $b=1$, $c=0$, $d=2$, $i=1$, $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 kernel value $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 defined by folding a fixed coupling list and summing a local contribution at each tuple. The comparison target $Z$ is an explicit piecewise integer table on the same six indices (sample entries include $4$, $-2$, and so on).
The module is chunk 13 of a 256-way case split: each chunk discharges one concrete six-tuple by kernel computation, so the global identity can later be assembled by exhaustive fin_cases. The local claim is exactly one point of that grid: indices $(3,1,0,2,1,1)$.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are fixed: the left-hand side evaluates the fold that defines $m_2^{\mathrm{num}}$, the right-hand side multiplies the table lookup for $Z$ by eight. No lemmas are invoked beyond kernel evaluation of those definitions.
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 proves it by six nested fin_cases over $\mathrm{Fin},4$, each leaf a chunk identity of this form. That global equality is the certified numerator identity in the Regge exact-midpoint $M_2$ TT analysis for 4D gravity.
Within Recognition Science gravity work, such kernel certificates underwrite discrete curvature bookkeeping on the eight-tick / $D=3$ side of the forcing chain; they do not themselves derive $G$ or the $\phi$-ladder, but they close a computational gap in the 4D midpoint expansion used downstream of those landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.