e_022203
plain-language theorem explainer
Pointwise kernel identity: the summed coupling numerator at index tuple (0,2,2,2,0,3) equals eight times the explicit integer table at those indices. Gravity analysts cite it only as one cell of the 4^6 case split that rebuilds the global m2Num = 8·explicitZ identity. Proof is a single kernel decide on two concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,2,2,2,0,3)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(0,2,2,2,0,3)=8\,Z_{\mathrm{expl}}(0,2,2,2,0,3)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification. The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a local contribution at each multi-index in $(\mathbb{F}4)^6$. The comparison object $Z{\mathrm{expl}}$ is an explicit integer-valued table on the same domain (pattern-matched closed form, e.g. values such as $4$, $-2$, and so on on distinguished index patterns).
The local goal of the chunk is the pointwise equality $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ on a block of the $4^6$ kernel cells. Module documentation states the chunk slogan directly: "$m2Num = 8\cdot explicitZ$, chunk 2 (256 kernel decides)." Upstream, both sides are pure definitions in the kernel certificate module; no analytic continuum limit is taken here.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values at the fixed six-tuple $(0,2,2,2,0,3)$, so the equality is a decidable integer comparison with no lemmas beyond the definitions of the folded numerator and the explicit table.
why it matters
This cell is consumed by the assembly theorem m2Num_eq_eight_explicitZ, which states the full universal claim $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and discharges it by exhaustive fin_cases on all six $\mathbb{F}_4$ coordinates. Each chunk theorem such as this one supplies one (or a block of) decided cells so the assembler can finish without re-deciding the whole kernel in one place.
In the broader gravity analysis stack, the identity is bookkeeping for the exact midpoint M2TT kernel in 4D Regge-type calculus: it certifies that the summed coupling numerator matches an eightfold multiple of a closed integer table, a finite combinatorial step rather than a continuum Einstein-equation derivation. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; those enter only if a later bridge maps this kernel into the RS gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.