e_033213
plain-language theorem explainer
Pointwise identity: the Regge midpoint numerator at multi-index (0,3,3,2,1,3) equals eight times the explicit integer kernel value at that same index. Gravity analysts cite it when discharging one cell of the 4D M2 TT kernel table. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,3,3,2,1,3)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 3 of a 256-cell kernel certification that the 4D Regge exact-midpoint numerator agrees with an explicit closed form: $m_2^{\mathrm{num}}=8\cdot Z$ at every multi-index in $(\mathrm{Fin},4)^6$.
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 term. The comparison target $Z$ is an explicit pattern-matched integer table on six $\mathrm{Fin},4$ indices (sample entries include $4$, $-2$, and so on).
The local setting is pure finite enumeration: no continuum limit, no physical units. Each chunk theorem pins one concrete six-tuple so the assembler can recombine them into the universal statement.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six indices are literals, so the kernel decision procedure closes the equality with no lemmas and no case split inside this declaration.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhausting all $\mathrm{Fin},4$ indices. That universal identity is the algebraic backbone of the Regge exact-midpoint M2 TT certification in 4D gravity analysis inside the monolith.
In the broader Recognition framework this sits in the gravity domain: it is bookkeeping that makes the discrete curvature/kernel identities machine-checkable, not a forcing-chain step (T5–T8) or an RCL identity. Its role is to remove a sorry-shaped gap in the 256-cell table so downstream curvature and continuum-matching arguments can quote a fully proved numerator identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.