e_233003
plain-language theorem explainer
For the six-index slot (2,3,3,0,0,3) 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 decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}3$, $c{=}3$, $d{=}0$, $i{=}0$, $j{=}3$ in $\{0,1,2,3\}$, the integer $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding the coupling list equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
In the Regge exact-midpoint 4D analysis, two integer kernels on six 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 term. The comparison target is an explicit piecewise integer table $Z$ on the same six indices (sample values include $4$, $-2$, and so on for listed patterns).
The module is chunk 11 of a 256-case kernel certification: each concrete sextuple is discharged separately so the global identity can be assembled by exhaustive case split. The local claim is exactly one cell of that grid: indices $(2,3,3,0,0,3)$.
proof idea
One-line kernel decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are fixed, so decide closes the equality with no further lemmas. No algebraic rewriting beyond evaluation of m2Num and explicitZ at this point.
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}}=8Z$ and proves it by nested fin_cases over all six indices, invoking one chunk equality per cell. Without these pointwise decides, the 4D Regge midpoint $M_2$ TT identity cannot be certified at the integer-kernel layer.
In the broader gravity stack this is bookkeeping infrastructure for the exact midpoint identity, not a new physical law. It sits downstream of the kernel certificate definitions and upstream of the assembled equality used by higher Regge analysis. No Recognition forcing-chain landmark (T5–T8, RCL, $\phi$) is directly at stake; the stake is mechanical completeness of the 256-cell table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.