e_301111
plain-language theorem explainer
One of 256 kernel identities equating the midpoint Regge mass-squared numerator at multi-index (3,0,1,1,1,1) to eight times the explicit integer kernel value at the same index. Gravity analysts assembling the exact 4D midpoint M2TT identity cite it as a discharged case. Proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,0,1,1,1,1)$ with each coordinate in $\{0,1,2,3\}$, the folded midpoint mass-squared numerator $m_2^{\mathrm{num}}$ equals eight times the explicit integer kernel $Z$: $m_2^{\mathrm{num}}(3,0,1,1,1,1)=8\,Z(3,0,1,1,1,1)$.
background
In the 4D Regge midpoint analysis, the mass-squared numerator is assembled by folding a fixed coupling list: each term contributes an integer depending on six Fin-4 indices, and the fold sum is $m_2^{\mathrm{num}}(a,b,c,d,i,j)$. Parallel to that sum sits an explicit integer table $Z$ on the same six-index domain, hard-coded by pattern match (e.g. $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and so on).
The local module is chunk 12 of the 256-case kernel certification that $m_2^{\mathrm{num}}=8Z$ pointwise. The full universal statement is proved downstream by exhaustive fin_cases on all six indices, each leaf a decide of this form. Indices live in $\mathrm{Fin},4$, matching the four discrete midpoint slots of the 4D Regge skeleton.
proof idea
One-line kernel proof: by decide. Both sides are closed integer terms once the six concrete Fin-4 values are substituted into the fold definition of the numerator and the pattern-match definition of the explicit kernel, so the equality reduces to a decidable integer comparison with no further lemmas.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which asserts the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by casing on each coordinate and invoking the 256 chunk decides. That global equality is the algebraic core of the exact midpoint M2TT identity in 4D Regge gravity analysis: it converts the folded coupling sum into a simple multiple of the explicit kernel, clearing the numerator side of the mass-squared bookkeeping.
Within Recognition Science gravity work this is pure discrete linear algebra on the midpoint skeleton, not a forcing-chain step (T0–T8) or an RCL identity. It closes one leaf of the 256-case decide tree so the assembly proof has no sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.