e_331031
plain-language theorem explainer
For the index sextuple (3,3,1,0,3,1) on Fin 4, the folded M2 numerator equals eight times the explicit Z-kernel entry. Gravity analysts assembling the full Regge midpoint identity cite this as one of the 256 kernel cells in chunk 15. The proof is a single `decide` that evaluates both integer sides.
Claim. For indices $a{=}3$, $b{=}3$, $c{=}1$, $d{=}0$, $i{=}3$, $j{=}1$ in $\{0,1,2,3\}$, the midpoint $M_2$ numerator (fold of coupling contributions) equals $8$ times the explicit integer $Z$-kernel value at that sextuple.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator side folds a fixed coupling list: each term contributes an integer depending on the six indices, and the fold starts at 0. The explicit side is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and so on).
The module goal is the pointwise identity numerator $= 8\cdot$ explicit kernel, discharged in chunks of kernel decides rather than one giant case split. Chunk 15 holds 256 such cells; the present declaration is the cell at $(3,3,1,0,3,1)$.
Upstream, the numerator and the explicit table are pure definitions in the kernel certificate module; no analytic hypothesis is attached to either.
proof idea
One-line kernel proof: decide. Lean evaluates the fold that defines the numerator at $(3,3,1,0,3,1)$ and the pattern match that defines the explicit $Z$ entry, then checks the integer equality against the factor $8$. No lemmas are invoked beyond the decidability of integer equality on concrete values.
why it matters
The parent theorem is the universal statement that the $M_2$ numerator equals eight times the explicit $Z$ kernel for every sextuple in $(\mathrm{Fin},4)^6$. That assembler runs nested fin_cases on all six indices; each concrete residual goal is exactly one cell of the form proved here.
Within Recognition gravity, the identity certifies that the discrete Regge midpoint curvature bookkeeping matches the closed-form $Z$ table used downstream in 4D coupling analysis. It is pure computational scaffolding for that equality, not a dynamical law, but without the cell-by-cell coverage the assembler cannot close.
No forcing-chain landmark (T5–T8, RCL, $\phi$-ladder) is at stake; the result is local to the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.