e_321010
plain-language theorem explainer
For the six-tuple of 4D simplex indices (3,2,1,0,1,0), the folded coupling numerator equals eight times the explicit kernel value. Gravity analysts cite it when discharging one cell of the 4D Regge midpoint M2–TT identity. The proof is a single kernel decision on concrete integers.
Claim. For indices $a{=}3$, $b{=}2$, $c{=}1$, $d{=}0$, $i{=}1$, $j{=}0$ 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 maps on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is obtained by folding a fixed coupling list and summing local contributions at those indices. The explicit kernel $Z$ is a sparse case table of small integers (entries such as $4$, $-2$, and so on) that is meant to match the numerator after a universal factor of eight.
The module is one chunk of a 256-cell decide grid that checks the pointwise identity $m_2^{\mathrm{num}}=8Z$ on concrete index tuples. Chunk 14 isolates a block of those tuples so the full universal statement can be assembled by exhaustive case split on $\mathrm{Fin},4$.
proof idea
One-line kernel proof: decide evaluates both sides at the fixed indices $(3,2,1,0,1,0)$ and checks integer equality. No lemmas are invoked beyond the definitions of the folded numerator and the explicit kernel table.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by six nested fin_cases over $\mathrm{Fin},4$. Each chunk theorem such as this one discharges one concrete cell so the universal identity is a pure case tree rather than a symbolic expansion of the fold. In the gravity stack this identity is the algebraic certificate that the midpoint M2–TT kernel matches its closed-form table, a step toward exact 4D Regge curvature bookkeeping in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.