e_020031
plain-language theorem explainer
Pointwise kernel identity: the Regge midpoint numerator m2Num at multi-index (0,2,0,0,3,1) equals eight times the explicit closed form explicitZ at the same indices. Gravity analysts cite it only as one cell of the 4^6 case split that assembles the global m2Num = 8·explicitZ theorem. The proof is a pure decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,2,0,0,3,1)$ with each coordinate in $\{0,1,2,3\}$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-way kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ on every 6-tuple of $\mathrm{Fin},4$ indices. The setting is the exact midpoint analysis of a 4D Regge-type TT identity used in the gravity sector.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term evaluated at the six indices. The comparison target $Z$ (explicitZ) is a sparse integer table on $(\mathrm{Fin},4)^6$, with nonzero entries such as $4$ on diagonal pairs like $(0,0,1,1,2,2)$ and $-2$ on mixed pairs like $(0,0,1,2,1,2)$.
Both definitions live in the KernelCert module; this chunk only evaluates them at one concrete multi-index.
proof idea
One-line computational proof: decide. After the six Fin-4 arguments are substituted, both sides reduce to concrete integers (the fold for $m_2^{\mathrm{num}}$ and the pattern match for $Z$), and the kernel decision procedure checks equality. No lemmas beyond the two definitions are invoked.
why it matters
The parent theorem is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and is proved by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one cell of that case tree.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint TT kernel in 4D Regge analysis: it certifies that the folded coupling numerator matches the closed-form sparse table used downstream. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete linear-algebra certification inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.