e_330231
plain-language theorem explainer
Pointwise identity: the folded Regge numerator m2Num at multi-index (3,3,0,2,3,1) equals eight times the explicit kernel value explicitZ at the same index. Gravity analysts cite it as one cell of the 256-case kernel certification that m2Num = 8·explicitZ. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,3,0,2,3,1)$ with each entry in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(3,3,0,2,3,1)$ equals $8$ times the explicit integer kernel $Z(3,3,0,2,3,1)$.
background
In the 4D Regge midpoint analysis, the TT-sector mass-squared numerator is assembled by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums contrib terms over couplingZList at six Fin-4 indices. The companion table explicitZ is a closed-form integer pattern on the same six indices (sample clauses give values such as $4$, $-2$, and so on).
The local module is chunk 15 of the certification that $m_2^{\mathrm{num}}=8\cdot Z$ holds at every kernel point. Upstream definitions live in the KernelCert module: m2Num is the fold, explicitZ is the pattern-matched table. The ambient goal is an exact algebraic identity for the midpoint Regge operator in four dimensions, not a continuum limit statement.
proof idea
One-line computational proof: by decide. Both sides are closed integer expressions once the six Fin-4 arguments are substituted, so the kernel decision procedure evaluates the fold defining $m_2^{\mathrm{num}}$ and the matching clause of $Z$, then checks equality to $8Z$. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges the claim by exhaustive Fin-case split. Each chunk such as this one pins a single multi-index so the global identity is a finite, machine-checked table rather than an opaque simplification. In the Recognition gravity stack this underwrites the exact midpoint TT identity used downstream in the 4D Regge analysis; it is bookkeeping infrastructure, not a new physical law, but without the pointwise cells the assembly theorem does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.