e_012100
plain-language theorem explainer
For the single index sextuple (0,1,2,1,0,0) on Fin 4, the Regge midpoint numerator m2Num equals eight times the explicit kernel table explicitZ. Gravity analysts cite it as one atomic case in the 4D M2TT identity. The proof is a pure kernel decide on the two integer definitions.
Claim. For the indices $(a,b,c,d,i,j)=(0,1,2,1,0,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(0,1,2,1,0,0)$ equals $8$ times the explicit integer kernel value $Z(0,1,2,1,0,0)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity: the claim that the folded numerator m2Num equals eight times a closed-form integer table explicitZ, discharged by 256 kernel decides.
m2Num a b c d i j is defined by folding contrib over couplingZList, accumulating an Int. explicitZ is a pattern-matched table on six Fin 4 indices, returning fixed integers such as $4$, $-2$, and so on for the nonzero support.
The local setting is pure finite enumeration: every sextuple in $(\mathrm{Fin},4)^6$ is a separate equality, later reassembled by exhaustive fin_cases.
proof idea
One-line kernel proof: by decide. Lean reduces both sides of m2Num 0 1 2 1 0 0 = 8 * explicitZ 0 1 2 1 0 0 to concrete integers (the fold of contrib versus the table entry times eight) and checks equality by the decidable instance on Int. No lemmas beyond the two definitions are invoked.
why it matters
This atom is consumed by m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by nested fin_cases over all six Fin 4 indices. Each chunk theorem such as e_012100 supplies one branch of that case split.
In the Recognition gravity stack the identity certifies that the midpoint Regge curvature numerator collapses to an explicit sparse kernel, a computational prerequisite for exact 4D discrete Einstein identities rather than a floating-point check. It does not itself touch the forcing chain (T0–T8) or the J-cost; it is infrastructure under the discrete gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.