e_332010
plain-language theorem explainer
Pointwise identity: the midpoint Regge m2 numerator at multi-index (3,3,2,0,1,0) equals eight times the explicit kernel integer Z at that index. Gravity analysts assembling the 4D TT midpoint identity cite these 256 kernel cells. The proof is a single kernel decide on two concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,3,2,0,1,0)$ with each entry in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 15 of a 256-cell kernel certification that the midpoint Regge $m_2$ numerator equals eight times an explicit integer table on $(\mathbb{F}_4)^6$. The ambient setting is the 4D transverse-traceless midpoint identity in discrete gravity (Regge calculus style analysis).
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling triple at the six indices. The explicit kernel $Z$ is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a finite case table (typical nonzero values include $4$, $-2$, and symmetric permutations).
Upstream, both $m_2^{\mathrm{num}}$ and $Z$ live in the kernel certificate module; this chunk only evaluates one concrete cell of the equality $m_2^{\mathrm{num}}=8Z$.
proof idea
One-line kernel proof: decide. Both sides reduce to closed integer expressions once the six Fin 4 arguments are literal, so the equality is a decidable Int fact with no further lemmas.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles all 256 cells by exhaustive fin_cases on $(a,b,c,d,i,j)$ and dispatches each cell to a chunk identity of this form. Without the pointwise facts, the universal statement that the folded numerator is exactly eight times the explicit kernel cannot close.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact 4D midpoint TT identity, not a new physical law. It sits downstream of the discrete coupling table and upstream of the assembled numerator identity used in Regge/TT analysis. No forcing-chain landmark (T5–T8, RCL, $\varphi$) is at stake here; the stake is certificate completeness of the integer kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.