e_310011
plain-language theorem explainer
For the Fin-4 index tuple (3,1,0,0,1,1), the folded midpoint mass-squared numerator equals eight times the explicit integer kernel value. Gravity analysts certifying the 4D Regge midpoint M2TT identity cite this as one decided cell in chunk 13 of the 256-kernel sweep. Proof is a single kernel `decide` on the two Int expressions.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,0,1,1)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator at those indices equals $8$ times the explicit integer kernel value at the same indices.
background
In the 4D Regge midpoint analysis the mass-squared numerator is an integer obtained by folding a fixed coupling list and summing a contribution function at six coordinates in $\mathrm{Fin},4$. The companion explicit kernel is a pattern-matched table on the same six-index domain, returning small integers (for example $4$ on certain matched pairs and $-2$ on selected off-diagonal patterns).
This module is chunk 13 of a decide sweep whose module doc states the goal as numerator $= 8\cdot$ explicit kernel across 256 cells. Both sides are pure Int-valued definitions, so each fixed tuple is a finite arithmetic check with no analytic hypotheses.
proof idea
One-line kernel decision. Lean evaluates the fold that defines the numerator and the pattern match that defines the explicit kernel at the concrete indices $(3,1,0,0,1,1)$, multiplies the latter by $8$, and accepts the integer equality by decide. No intermediate lemmas are invoked.
why it matters
The cell feeds the assembler theorem that states the identity for every six-tuple in $\mathrm{Fin},4$, discharged there by exhaustive fin_cases on the six indices. That universal equality is part of the exact midpoint M2TT certification stack in the gravity analysis layer. The result is discrete kernel bookkeeping only: it does not touch the T0–T8 forcing chain, the Recognition Composition Law, or the $\varphi$-ladder mass formula, but it underwrites the algebraic side of the Regge midpoint identities used higher in the gravity modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.