e_021100
plain-language theorem explainer
Pointwise kernel check: the folded M2 numerator at multi-index (0,2,1,1,0,0) equals eight times the explicit Z table value there. Gravity analysts assembling the 4D Regge midpoint TT identity cite this as one of the 256 decide-chunks. Proof is a single kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,1,0,0)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer table on those indices.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathbb{F}_4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at $(a,b,c,d,i,j)$. The comparison target $Z$ is an explicit case table of small integers (entries such as $4$, $-2$, and so on) on the same index domain.
This module is chunk 2 of a 256-way split of the kernel identity $m_2^{\mathrm{num}}=8Z$. Each chunk theorem pins one concrete multi-index so the assembler can recombine them by exhaustive fin_cases on $\mathbb{F}_4^6$.
proof idea
One-line proof: decide. Both sides reduce to concrete Int values at the fixed indices $(0,2,1,1,0,0)$ (left via the fold definition of $m_2^{\mathrm{num}}$, right via the case table for $Z$), and the kernel checks the equality $n=8m$ by computation.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by six nested fin_cases over $\mathbb{F}_4$, dispatching each cell to a chunk such as this one.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2/TT kernel in 4D Regge calculus: it certifies that the folded coupling numerator matches the closed-form $Z$ table up to the universal factor $8$. That factor is the combinatorial normalization used when the continuum or continuum-limit identities are recovered from the discrete kernel. No forcing-chain landmark (T5–T8) is touched directly; the result is pure discrete-gravity algebra inside the RS gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.