e_120110
plain-language theorem explainer
Single kernel case: the midpoint M2 numerator at index sextuple (1,2,0,1,1,0) equals eight times the explicit Z-coupling there. Gravity analysts assembling the 4D Regge midpoint identity cite it as one of 256 concrete decides. The proof is a pure computational `decide` on fixed integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,0,1,1,0)$ in $(\mathrm{Fin}\,4)^6$, the midpoint $M_2$ numerator equals eight times the explicit integer $Z$-coupling at those indices: $m_2^{\mathrm{num}}(1,2,0,1,1,0)=8\,Z_{\mathrm{expl}}(1,2,0,1,1,0)$.
background
In the 4D Regge midpoint analysis, the numerator of the discrete $M_2$ mass-like term is assembled by folding a fixed coupling list: each triple contributes an integer contrib, and the fold yields an Int for every sextuple of face/edge indices in $\mathrm{Fin},4$. The companion table explicitZ is a sparse case-split that records the closed-form integer expected at each sextuple (e.g. $4$, $-2$, and zeros elsewhere).
The local module is chunk 6 of a 256-way partition of the kernel: each chunk discharges a block of concrete equalities $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ by native decision, so the universal quantifier can later be rebuilt by exhaustive fin_cases without re-running the fold at assemble time.
Upstream, m2Num is exactly that fold over couplingZList; explicitZ is the hand-written target table. The factor eight is the combinatorial multiplicity that converts the raw coupling sum into the normalized midpoint weight used by the TT-identity certificate.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals, so the kernel equality checker closes the goal with no lemmas and no arithmetic rewriting.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by six nested fin_cases that invoke one chunk theorem per cell. That universal identity is the algebraic core of the 4D Regge exact-midpoint TT certificate: it replaces a symbolic fold by a closed integer table, letting curvature and mass terms cancel exactly on the midpoint lattice.
Within Recognition gravity, the certificate sits in the discrete-geometry layer that underwrites continuum limits and the effective Newtonian sector; the eight-factor itself echoes the eight-tick octave (T7) combinatorial bookkeeping, though this lemma only records the integer identity, not the continuum limit. No open scaffold remains on this cell: the decide is complete.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.