e_302002
plain-language theorem explainer
Pointwise identity: the Regge midpoint mass-squared numerator at multi-index (3,0,2,0,0,2) equals eight times the explicit Z-kernel entry there. Gravity analysts cite it as one of 256 kernel cells in the 4D midpoint M2–TT identity. The proof is a single kernel decision (`decide`) on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,0,2,0,0,2)$ with each coordinate in $\{0,1,2,3\}$, the folded mass-squared numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 12 of a 256-cell kernel certification that the 4D Regge midpoint mass-squared numerator equals eight times an explicit integer kernel $Z$. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels ${0,1,2,3}$ on a 4-simplex edge/face pattern.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a coupling list: it sums contribution terms contrib over couplingZList at the six indices. The comparison target explicitZ is a closed-form integer table on those same six $\mathrm{Fin},4$ arguments (sample clauses give values such as $4$, $-2$, and so on).
The local claim is only the single cell $(3,0,2,0,0,2)$. Sibling theorems cover the other cells; the assemble module quantifies over all six indices.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete multi-index to integers (the fold that defines the numerator, and the matching clause of the explicit $Z$ table) and checks equality by the kernel decision procedure. No lemmas are invoked beyond the definitions of the numerator and the explicit kernel.
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,Z$ on $\mathrm{Fin},4^6$. That universal identity is the certified algebraic core of the 4D Regge midpoint M2–TT relation used in the gravity analysis stack.
In Recognition Science terms this is bookkeeping inside the discrete gravity sector (Regge calculus on the recognition complex), not a T0–T8 forcing step. It closes one of the 256 decide cells so the assemble proof can treat the numerator/kernel ratio as an identity rather than a hypothesis. Open scaffolding elsewhere in gravity still depends on having every cell discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.