e_311101
plain-language theorem explainer
Single index identity: the midpoint mass-squared numerator at Fin-4 indices (3,1,1,1,0,1) equals eight times the explicit Z coupling there. Gravity analysts cite it as one cell of the 256-case kernel that certifies m2Num = 8·explicitZ. The proof is a pure kernel decision (`decide`).
Claim. For indices $(a,b,c,d,i,j)=(3,1,1,1,0,1)$ in $(\mathrm{Fin}\,4)^6$, the midpoint $m^2$ numerator equals eight times the explicit integer $Z$-coupling at those indices: $m_2^{\mathrm{num}}(3,1,1,1,0,1)=8\,Z(3,1,1,1,0,1)$.
background
This module is chunk 13 of the 256 kernel decides that establish the algebraic identity $m_2^{\mathrm{num}}=8\cdot Z$ on all of $(\mathrm{Fin},4)^6$. The setting is the exact midpoint analysis of the 4D Regge mass-squared numerator used in the Recognition Science gravity stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at the six indices. The comparison object $Z(a,b,c,d,i,j)$ is an explicit integer-valued table on the same domain (sample values include $4$, $-2$, and so on for distinguished index patterns).
Both definitions live in the kernel certificate module; this chunk only evaluates one concrete six-tuple.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the equality at the concrete Fin-4 literals $(3,1,1,1,0,1)$ and checks integer equality in the kernel. No lemmas are invoked beyond the unfoldings of $m_2^{\mathrm{num}}$ and $Z$.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhausting cases. That global equality is the certified link between the folded coupling-sum definition of the midpoint $m^2$ numerator and the closed-form explicit $Z$ table used downstream in the Regge gravity analysis.
Within Recognition Science gravity work, these kernel cells underwrite exact midpoint identities rather than approximate continuum limits. The chunking (256 decides) keeps each goal tiny and machine-checkable while the assembler rebuilds the full $\forall$ statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.