e_222222
plain-language theorem explainer
For the six Fin-4 indices all equal to 2, the discrete M2 numerator equals eight times the explicit Z kernel value. Case-split assemblers of the 4D Regge midpoint identity cite this as one of the 256 kernel cells. Proof is a single decide evaluating both concrete integer sides.
Claim. For indices $a=b=c=d=i=j=2$ in $\{0,1,2,3\}$, the M2 numerator satisfies $m_2^{\mathrm{num}}(2,2,2,2,2,2)=8\,Z_{\mathrm{expl}}(2,2,2,2,2,2)$.
background
In the 4D Regge exact-midpoint analysis, the M2 numerator is an integer obtained by folding a fixed coupling list: each term adds a contribution depending on a coupling triple and six Fin-4 indices. The explicit Z kernel is a closed-form integer function on the same six indices, sparse and pattern-matched (values such as 4 or -2 on selected slots, zero elsewhere).
This module is chunk 10 of the case-by-case check that the numerator always equals eight times that kernel. The setting is pure Fin-4 integer arithmetic; no continuum limit or physical units enter here. Upstream, both sides are already defined as total functions on Fin 4.
proof idea
One-line wrapper: decide. With all six indices fixed at 2, both sides reduce to concrete integers (left: the fold that defines the M2 numerator; right: eight times the pattern-matched explicit Z entry). The kernel decides equality of those two integers. No lemmas beyond the two definitions are invoked.
why it matters
Supplies one cell of the universal identity assembled downstream as m2Num_eq_eight_explicitZ, which states that for every six-tuple of Fin-4 indices the numerator equals eight times explicit Z, proved by exhaustive fin_cases on all six arguments. That parent identity is the certified discrete kernel for the 4D Regge midpoint M2 structure in the gravity analysis layer. It does not touch the T0–T8 forcing chain, J-uniqueness, or the phi ladder; it is infrastructure so the discrete coupling matches the intended continuum limit bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.