e_203212
plain-language theorem explainer
For multi-index (2,0,3,2,1,2) in Fin 4, the folded M₂ numerator equals eight times the explicit integer kernel entry. Analysts assembling the 4D Regge midpoint M₂-TT identity cite this as one discrete case among the 4⁶ kernel. Proof is a single kernel decide on the concrete integer equality.
Claim. For indices $a{=}2$, $b{=}0$, $c{=}3$, $d{=}2$, $i{=}1$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded 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 Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a contribution function over a fixed coupling list:
$$m_2^{\mathrm{num}}(a,b,c,d,i,j)=\sum_{t\in\mathrm{couplingZList}}\mathrm{contrib}(t;a,b,c,d,i,j).$$
The companion table $Z$ is an explicit pattern-matched Int on the same six indices (sample clauses give values such as $4$, $-2$, etc.). The module goal is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$, discharged by 256 kernel decides per chunk; this file is chunk 8 of that enumeration.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(2,0,3,2,1,2)$ 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 universal assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and is proved by exhaustive fin_cases on all six indices. Each chunk theorem such as this one closes one concrete cell of that $4^6$ grid. In the broader Gravity/Regge strand this identity is the algebraic certificate that the midpoint M₂-TT coupling matches eight copies of the explicit kernel, a step toward the discrete curvature bookkeeping used in the Recognition gravity analysis. It does not itself touch the T0–T8 forcing chain or the J-cost; it is pure kernel arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.