e_210301
plain-language theorem explainer
Single multi-index identity: the Regge midpoint m₂ numerator at (2,1,0,3,0,1) equals eight times the explicit integer kernel Z at that sextuple. Gravity analysts cite it as one kernel cell in the 4D midpoint TT identity. The proof is a pure `decide` on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,3,0,1)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on sextuples of Fin 4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib, and the fold starts at 0. The comparison target is an explicit table explicitZ, a pattern-matched function Fin 4^6 → ℤ with sparse nonzero entries (e.g. 4 on matched diagonal pairs, −2 on certain off-diagonal swaps).
This module is chunk 9 of a partitioned kernel certification whose module doc states the global claim $m_2^{\mathrm{num}}=8\cdot Z$, discharged by 256 concrete decides. The present declaration fixes one sextuple inside that partition. Upstream, only the two kernel definitions are required; no analytic lemma about Regge calculus is invoked at this layer.
proof idea
One-line computational proof: by decide. After the six Fin 4 arguments are substituted, both sides reduce to concrete integers (the fold for the numerator versus eight times the matched explicitZ clause, or zero if unmatched). Lean’s decision procedure checks integer equality; no rewriting or intermediate lemmas appear.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts the identity for every sextuple in Fin 4 by exhausting cases. That global equality is the algebraic core of the exact midpoint M₂ TT identity in the 4D Regge analysis used on the gravity side of the Recognition stack. Chunk theorems like this one keep the kernel certification modular and machine-checkable without a closed-form summation argument. They do not themselves touch the forcing chain (T0–T8), φ, or the eight-tick octave; they sit downstream as discrete curvature-bookkeeping support for the continuum gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.