e_032001
plain-language theorem explainer
At multi-index (0,3,2,0,0,1) the folded Regge midpoint numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts cite this as one of the 256 concrete kernel points that assemble the full m2Num = 8·explicitZ identity. The proof is a single decide on fixed Fin-4 arguments.
Claim. For indices $(a,b,c,d,i,j)=(0,3,2,0,0,1)$ in $(\mathbb{F}_4)^6$, 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
This module is chunk 3 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on all of $(\mathbb{F}_4)^6$. The ambient setting is the exact midpoint identity for the 4D Regge TT mass-squared numerator in the Recognition gravity analysis stack.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution contrib t a b c d i j. The comparison target explicitZ is a closed integer table on six $\mathbb{F}_4$ indices (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and several $-2$ off-diagonal patterns).
Both objects live in the kernel certificate module imported here; the chunk theorems only evaluate them at concrete points.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,3,2,0,0,1)$ and checks integer equality. No lemmas are invoked beyond the decidable arithmetic of Int and the concrete definitions of m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every index sextuple by nested fin_cases and lands on these chunk equalities. Without the pointwise facts, the global identity $m_2^{\mathrm{num}}=8\cdot Z$ does not close.
In the gravity stack this identity is the algebraic certificate that the midpoint TT numerator matches the explicit kernel used downstream in Regge curvature bookkeeping. It is pure discrete linear algebra on $\mathbb{F}_4$ indices, not a continuum GR claim, and sits inside the Recognition gravity analysis path rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.