e_223203
plain-language theorem explainer
For the concrete Fin-4 indices (2,2,3,2,0,3), the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts assembling the full Regge midpoint M2 identity cite this as one of 256 kernel cells. The proof is a single decide on closed integer arithmetic.
Claim. For indices $a{=}2$, $b{=}2$, $c{=}3$, $d{=}2$, $i{=}0$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel integer: $m_2^{\mathrm{num}}(2,2,3,2,0,3)=8\,Z_{\mathrm{expl}}(2,2,3,2,0,3)$.
background
This module is chunk 10 of a 256-cell kernel certification that the Regge-exact midpoint numerator equals eight times an explicit integer table on every sextuple of $\mathrm{Fin},4$ indices. The ambient setting is 4D discrete gravity analysis: couplings are summed, then matched against a closed-form kernel.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and adding each term's contribution at those indices. The comparison table $Z_{\mathrm{expl}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern match (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local claim is only the single cell $(2,2,3,2,0,3)$; sibling theorems cover the rest of the chunk.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the fold for the numerator and the pattern match for the explicit kernel are evaluated at the six literal Fin 4 arguments, so the equality is a closed Int fact discharged by the decision procedure. No lemmas beyond the two definitions are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by nested fin_cases on all six indices. Each leaf is exactly a cell theorem of this form; this declaration supplies the $(2,2,3,2,0,3)$ leaf inside chunk 10.
In the Recognition gravity stack, that universal identity is the certified algebraic core of the Regge-exact midpoint M2/TT analysis in 4D. It does not itself invoke the forcing chain (T5–T8) or the RCL, but it is infrastructure those continuum limits sit on: without the numerator–kernel match, the discrete curvature bookkeeping does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.