e_110100
plain-language theorem explainer
Pointwise identity: the midpoint Regge m₂ numerator at index sextuple (1,1,0,1,0,0) equals eight times the explicit Z-kernel entry there. Gravity analysts cite it as one cell of the 256-case kernel that underwrites m₂Num = 8·explicitZ on all Fin-4 arguments. The proof is a single kernel decide on closed integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(1,1,0,1,0,0)$ in $(\mathrm{Fin}\,4)^6$, the midpoint $m_2$ numerator equals eight times the explicit integer $Z$-kernel value: $m_2^{\mathrm{num}}(1,1,0,1,0,0)=8\,Z_{\mathrm{expl}}(1,1,0,1,0,0)$.
background
This module is chunk 5 of a 256-way case split proving that the folded midpoint $m_2$ numerator coincides with eight times a hand-tabulated integer kernel on every sextuple of $\mathrm{Fin},4$ indices. The setting is 4D Regge calculus at the exact midpoint configuration used in the Recognition gravity analysis.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing local contributions at those six indices. The comparison table $Z_{\mathrm{expl}}$ is an explicit pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample clauses include values $4$, $-2$, and so on for distinguished index patterns).
The global claim assembled downstream is $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$. Each chunk theorem discharges one concrete sextuple so the assembler can finish by exhaustive fin_cases.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six indices are substituted into the fold definition of the numerator and the pattern match of the explicit kernel; Lean’s decision procedure checks equality in $\mathbb{Z}$. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $\mathrm{Fin},4$ sextuple by nested fin_cases and invokes each chunk cell such as this one. That global equality is the certified bridge between the folded coupling definition of the midpoint $m_2$ numerator and the compact explicit $Z$ table used in the 4D Regge midpoint analysis.
In the Recognition gravity stack this closes a purely algebraic kernel obligation: once numerator and table agree everywhere, downstream curvature and mass-side identities can quote the eight-fold multiple without re-expanding the fold. It is bookkeeping, not a new physical law, but the audit trail for the midpoint $m_2$ identity depends on every cell being decided.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.