e_310121
plain-language theorem explainer
For the six-index slot (3,1,0,1,2,1) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact 4D Regge midpoint M2TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the midpoint numerator $m_2^{\mathrm{num}}(3,1,0,1,2,1)$ equals $8\,Z(3,1,0,1,2,1)$, where $Z$ is the explicit integer kernel table and $m_2^{\mathrm{num}}$ is the fold of coupling contributions over that table.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices appear. The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: each term contributes an integer contrib, and the fold starts at zero. The companion map $Z$ (explicitZ) is a sparse lookup table of small integers (entries such as $4$, $-2$, and so on) that is meant to be the closed form of that fold, up to a universal factor of eight.
This module is chunk 13 of a 256-cell kernel certification: each cell fixes one concrete six-tuple and asserts $m_2^{\mathrm{num}}=8Z$ at that point. The local setting is pure integer arithmetic on a finite index set; no continuum limit or physical units enter the statement.
proof idea
One-line decide proof. Both sides reduce to concrete Int values once the six Fin-4 arguments are substituted: the left-hand side evaluates the fold that defines $m_2^{\mathrm{num}}$, the right-hand side multiplies the table entry of $Z$ by eight. Lean’s kernel decision procedure checks integer equality and closes the goal.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the identity for every six-tuple by exhaustive fin_cases on all six indices; each case discharges to one of these chunk lemmas (here the cell $(3,1,0,1,2,1)$). Without the full 256-cell cover, the exact midpoint M2TT numerator identity in 4D Regge calculus remains uncertified. In the Recognition gravity stack this is bookkeeping infrastructure for the discrete curvature/mass side, not a forcing-chain landmark (T5–T8), but it is required before continuum or phenomenological claims that quote the closed-form kernel can be trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.