e_021123
plain-language theorem explainer
Kernel-checked equality of the folded Regge numerator against eight times the closed-form table at the single index sextuple (0,2,1,1,2,3). Gravity analysts cite it only as one cell of the 256-case cover that assembles the universal m2Num = 8·explicitZ identity. The proof is a one-line decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}1$, $d{=}1$, $i{=}2$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(0,2,1,1,2,3)$ equals $8$ times the explicit closed-form integer $Z(0,2,1,1,2,3)$.
background
In the 4D Regge midpoint analysis the integer kernel of the second-moment TT identity is written two ways. The folded form $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums every contribution from a fixed coupling list over the six $\mathrm{Fin},4$ indices. The closed form $\mathrm{explicitZ}$ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and so on) on the same six-index domain.
The local module is chunk 2 of a 256-case partition: each chunk discharges a block of concrete sextuples by kernel decision, so that a later assembler can reassemble the universal identity by exhaustive $\mathrm{fin_cases}$. The two upstream definitions supply exactly the left- and right-hand sides compared here.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple $(0,2,1,1,2,3)$ and checks integer equality. No lemmas are invoked; the kernel reduces the fold that defines the numerator and the pattern match that defines the closed form to bare integers and compares them.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and proves it by six nested $\mathrm{fin_cases}$ over $\mathrm{Fin},4$, each leaf landing on one of these chunk equalities. Without the full 256-cell cover the universal identity does not close.
In the broader Recognition gravity stack that identity is the algebraic certificate that the midpoint Regge second-moment kernel matches its closed form, a prerequisite for exact 4D TT projections used downstream in the discrete curvature analysis. It is pure integer bookkeeping, not a dynamical claim about $G$ or the $\phi$-ladder, but it is load-bearing scaffolding for those later steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.