e_022331
plain-language theorem explainer
At the fixed multi-index (0,2,2,3,3,1), the Regge midpoint M2 numerator equals eight times the explicit Z-factor. Gravity analysts auditing the 4D midpoint TT identity cite this as one cell of the chunk-2 kernel table. The proof is a pure kernel decision: both sides are closed integer expressions, discharged by decide.
Claim. For the multi-index $(0,2,2,3,3,1)$, the midpoint $M_2$ numerator equals eight times the explicit $Z$ value at that point: $N_{M_2}(0,2,2,3,3,1)=8\,Z_{\mathrm{expl}}(0,2,2,3,3,1)$.
background
This module sits in the Gravity analysis layer that certifies an exact midpoint identity for the Regge $M_2$ TT sector in four dimensions. The local contract, stated in the module header, is that the numerator $N_{M_2}$ equals eight times an explicit combinatorial $Z$ factor, checked cell-by-cell over a 256-entry kernel chunk.
The six integer arguments label a discrete multi-index into that kernel (edge/face or mode labels in the midpoint expansion). Sibling declarations in the same file cover the other cells of chunk 2; the imported kernel-cert module supplies the shared definitions of the numerator and of explicit $Z$ as decidable integer functions of those indices.
No analytic lemma is required at this layer: both sides reduce to concrete integers once the indices are fixed.
proof idea
One-line decision proof. After unfolding the definitions of the numerator and of explicit $Z$ at the constant indices $(0,2,2,3,3,1)$, both sides are closed arithmetic expressions in $\mathbb{Z}$. The decide tactic runs the kernel's decidable-equality procedure and closes the goal with no further lemmas.
why it matters
The parent goal of the chunk is the global identity $N_{M_2}=8,Z_{\mathrm{expl}}$ on the full 4D midpoint kernel. Each cell theorem such as this one discharges one multi-index so the chunk can be reassembled without gaps. In the Recognition gravity stack these kernel identities underwrite exact midpoint evaluations used in discrete curvature and TT-sector bookkeeping; they are infrastructure rather than a forcing-chain step (T0–T8), but they keep the Regge side free of floating-point or sorry-laden arithmetic. With empty upstream/downstream edges in the graph, the declaration is a leaf certificate inside chunk 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.