e_010301
plain-language theorem explainer
For the Fin-4 index sextuple (0,1,0,3,0,1), the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one cell of the 256-way case split that establishes the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,3,0,1)$ in $(\mathrm{Fin}\,4)^6$, the integer 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
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at the six Fin-4 indices, and the fold starts from 0. The comparison target is explicitZ, a piecewise integer table on $(\mathrm{Fin},4)^6$ (e.g. value 4 on diagonal pairs such as $(0,0,1,1,2,2)$, value $-2$ on mixed pairs such as $(0,0,1,2,1,2)$).
The local claim is the scalar equality $m_2^{\mathrm{num}}=8\cdot Z$ at one concrete sextuple. The module header states the program: prove $m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$ by 256 kernel decides, of which this is chunk-1 cell e_010301.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side by evaluating the fold that defines $m_2^{\mathrm{num}}$ at $(0,1,0,3,0,1)$, the right-hand side by looking up explicitZ at the same indices and multiplying by 8. Lean’s kernel decision procedure checks integer equality; no lemmas are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ by exhaustive fin_cases on all six indices. Each leaf of that case tree is one of these e_* decide theorems; without the cell for $(0,1,0,3,0,1)$ the universal identity does not close.
In the broader Gravity analysis stack this identity is the certified algebraic core of the Regge exact-midpoint $M_2$ TT relation in 4D: it replaces a summed coupling expression by a closed piecewise kernel, enabling downstream curvature and continuum-limit arguments. It is pure discrete linear algebra on Fin-4 indices, not a continuum GR derivation by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.