e_310300
plain-language theorem explainer
At multi-index (3,1,0,3,0,0) the Regge midpoint mass-squared numerator equals eight times the explicit Z-table value. Gravity analysts building the 4D midpoint M2TT identity cite this as one kernel case among the chunked enumeration. The proof is a single kernel `decide` on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,3,0,0)$ in $(\mathrm{Fin}\,4)^6$, 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 sits in the Gravity analysis layer that certifies an exact midpoint identity for a 4D Regge-style mass-squared numerator. The local claim of the file is the pointwise equality $m_2^{\mathrm{num}}=8\cdot Z$ on a 256-case chunk of the $(\mathrm{Fin},4)^6$ index space, discharged by kernel decision.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: each term contributes an integer contrib and the accumulator starts at 0. The comparison table $Z$ is an explicit six-index integer function on $\mathrm{Fin},4$, given by a large pattern-match (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both definitions live in the kernel-certificate module imported here. The present declaration fixes one concrete sextuple and asserts the scaled equality at that point only.
proof idea
One-line kernel proof: decide. After substituting the six concrete Fin 4 indices, both sides reduce to closed integer expressions (the fold for the numerator versus eight times the matched explicitZ clause), and the decidable equality on Int closes the goal with no lemmas or case splits in this file.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the full pointwise identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhausting $(\mathrm{Fin},4)^6$. This chunk entry is one of the named case facts that feed that assembly (chunk 13 in the module family).
In the Recognition gravity stack, the midpoint M2TT identity is bookkeeping for discrete curvature/mass-squared couplings on a 4-index combinatorial scaffold. Certifying numerator equals eight times the closed Z-table removes a large computational obligation from later continuum or continuum-limit arguments. It does not itself invoke the forcing chain (T5–T8), RCL, or the phi-ladder; it is pure finite-index integer algebra supporting the gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.