e_302020
plain-language theorem explainer
For the single multi-index (3,0,2,0,2,0) on Fin 4, the Regge midpoint mass-squared numerator equals eight times the explicit integer kernel value. Gravity analysts cite it as one cell of the 256-case kernel that builds the global identity m2Num = 8·explicitZ. The proof is a pure kernel decide on that fixed tuple.
Claim. With indices in $\{0,1,2,3\}$, the midpoint mass-squared numerator at $(a,b,c,d,i,j)=(3,0,2,0,2,0)$ equals $8$ times the explicit coupling kernel at the same indices: $N(3,0,2,0,2,0)=8\,Z(3,0,2,0,2,0)$.
background
In the 4D Regge midpoint analysis, the mass-squared numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing integer contributions at each multi-index in $(\mathrm{Fin},4)^6$. The companion map $Z$ is an explicit piecewise-integer kernel on the same domain (sample values include $4$, $-2$, and other small integers on diagonal and off-diagonal patterns).
The local module is chunk 12 of a 256-cell decide table whose sole job is to check $N=8Z$ pointwise. Upstream, $N$ is the fold of contributions and $Z$ is the closed-form table; neither is proved equal globally here, only evaluated at one concrete tuple.
The ambient goal is an exact algebraic identity in the discrete gravity kernel, not a continuum limit statement.
proof idea
One-line decide on the ground term m2Num 3 0 2 0 2 0 = 8 * explicitZ 3 0 2 0 2 0. Lean reduces both sides through the fold definition of the numerator and the pattern-match definition of the explicit kernel, then checks integer equality. No lemmas beyond those two definitions are invoked.
why it matters
This cell is consumed by the assembly theorem that states $\forall a,b,c,d,i,j,, N=8Z$, proved by exhaustive fin_cases over all six Fin-4 indices. Each chunk theorem such as this one discharges one branch of that case split, so the global midpoint mass-squared identity rests on the full 256-cell table.
In the Recognition gravity stack the identity certifies that the discrete TT midpoint kernel matches its closed-form integer expression, a prerequisite for exact (non-approximate) Regge mass-squared bookkeeping in 4D. It does not itself touch the forcing chain T0–T8 or the J-cost law; it is pure kernel arithmetic supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.