e_310212
plain-language theorem explainer
For the six-index slot (3,1,0,2,1,2) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over all 4^6 index tuples. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}1$, $c{=}0$, $d{=}2$, $i{=}1$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is one chunk in a 256-way case split proving that the Regge midpoint $M_2$ numerator equals eight times an explicit integer kernel on every 4D index tuple. The ambient setting is discrete gravity analysis: couplings on $\mathrm{Fin},4$ edges are folded into a single integer numerator.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each six-index slot. The companion $Z$ is an explicit pattern-matched integer table on $\mathrm{Fin},4^6$ (sample values include $4$, $-2$, and so on). The claim here is the numerical identity at one concrete slot, not the universal statement.
proof idea
One-line kernel proof: decide evaluates both sides as concrete Int values (the fold for $m_2^{\mathrm{num}}$ at $(3,1,0,2,1,2)$ and eight times the matched $Z$ entry) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the two sides.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which introduces all six $\mathrm{Fin},4$ variables and discharges every cell by fin_cases, routing each cell to a chunk theorem of this form. Without the per-cell identities, the global midpoint numerator identity cannot close.
In the gravity stack this is bookkeeping for the exact 4D Regge midpoint $M_2$ TT identity: once $m_2^{\mathrm{num}}=8Z$ holds everywhere, later analysis can replace the folded sum by the closed kernel. It is not itself a forcing-chain step (T0–T8); it is computational support inside the discrete gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.