e_210221
plain-language theorem explainer
Pointwise identity: the Regge midpoint m₂ numerator at multi-index (2,1,0,2,2,1) equals eight times the explicit Z table entry there. Gravity analysts cite it as one of the 256 kernel cells that assemble the full m₂Num = 8·explicitZ theorem. Proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,1,0,2,2,1)$ with each coordinate in $\{0,1,2,3\}$, the integer $m_2$ numerator equals eight times the explicit $Z$-table value at that multi-index: $m_2(2,1,0,2,2,1)=8\,Z(2,1,0,2,2,1)$.
background
This module is chunk 9 of a 256-cell kernel certification that the 4D Regge midpoint $m_2$ numerator coincides with eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels ${0,1,2,3}$ on a 4-simplex edge/face pattern.
The numerator $m_2\mathrm{Num}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at those six indices. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample entries include $4$, $-2$, and so on for the listed index patterns).
Local setting (module doc): prove $m_2\mathrm{Num}=8\cdot\mathrm{explicitZ}$ cell by cell via kernel decides, then reassemble.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed literals: the fold that defines the numerator evaluates fully, the table lookup for explicit $Z$ fires its matching clause (or default), and the kernel checks equality of the resulting Int values. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by exhausting indices with fin_cases. Each chunk cell such as this one discharges one concrete goal in that 256-way split.
In the Recognition gravity stack this is bookkeeping for the exact midpoint Regge identity in 4D: the numerator that enters the discrete curvature/mass side is forced to match an explicit sparse integer kernel, scaled by 8. It does not itself touch the forcing chain (T0–T8) or the J-cost, but it is part of the certified discrete-gravity substrate those continuum limits sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.