e_020020
plain-language theorem explainer
Pointwise identity: the midpoint M2 TT numerator at multi-index (0,2,0,0,2,0) equals eight times the explicit integer Z-table entry. Gravity analysts cite it when assembling the full 4D kernel identity m2Num = 8·explicitZ. Proof is a single kernel decide on concrete Fin-4 data.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,0,2,0)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing local contributions at $(a,b,c,d,i,j)$. The companion table $Z$ is an explicit case-split function returning small integers (typically $\pm 2,\pm 4$, or $0$ off the listed patterns).
The module is chunk 2 of a 256-way partition of the Fin-4^6 domain. Each chunk theorem asserts $m_2^{\mathrm{num}}=8Z$ at one concrete multi-index so the global identity can be reassembled by exhaustive fin_cases without a single giant decide.
Upstream, $Z$ and $m_2^{\mathrm{num}}$ live in the kernel certificate module; this file only discharges one coordinate of their equality.
proof idea
One-line proof: decide. Both sides are closed integer terms once the six Fin-4 arguments are literals, so the kernel evaluates the fold defining $m_2^{\mathrm{num}}$ and the case table for $Z$, then checks equality to $8Z$. No lemmas are invoked beyond computational reduction.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ by six nested fin_cases over the chunk lemmas (including this one). That global identity is the algebraic core of the Regge exact midpoint M2 TT certificate in 4D: it replaces an opaque summed coupling by a sparse explicit integer table, making curvature and deficit bookkeeping checkable by computation.
Within Recognition gravity, this sits in the discrete geometric layer that supports continuum limits and effective Newtonian recovery; it does not itself invoke the forcing chain (T5–T8) or the J-cost, but it hardens the 4D combinatorial skeleton those continuum claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.