e_010103
plain-language theorem explainer
At multi-index (0,1,0,1,0,3), the Regge midpoint M2 numerator equals eight times the explicit Z kernel entry. Gravity analysts cite this as one atomic case in the 4D TT-identity certification. The proof is a single kernel decision (`decide`) on concrete integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,1,0,3)$ 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
This module sits in the 4D Regge gravity analysis that certifies an exact midpoint identity for the M2 TT sector. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer depending on six $\mathrm{Fin},4$ indices, and the fold starts from zero. The comparison target is an explicit piecewise kernel $Z$ on the same six indices, tabulated by pattern (for example $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and so on).
The local goal, stated in the module header, is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on a 256-point chunk of the index cube, discharged by kernel decides rather than by a closed algebraic argument. This declaration is the single point $(0,1,0,1,0,3)$ inside that chunk.
proof idea
One-line computational proof: decide evaluates both sides on the concrete six-tuple. The left side runs the fold that defines the numerator; the right side looks up (or reduces to) the explicit kernel value and multiplies by eight. No lemmas are invoked beyond the definitions of the numerator and the kernel.
why it matters
The parent assembly theorem states the full quantified claim: for every six-tuple in $(\mathrm{Fin},4)^6$, the numerator equals eight times the explicit kernel. Its proof is nested fin_cases over all six indices; each leaf is a point check of this form. This declaration supplies the leaf at $(0,1,0,1,0,3)$ inside chunk 1.
In the broader Recognition gravity stack, the identity is infrastructure for the exact midpoint Regge M2 TT analysis in four dimensions. It does not itself invoke the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$), but it is part of the discrete geometric bookkeeping those continuum limits rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.