e_130232
plain-language theorem explainer
For the index sextuple (1,3,0,2,3,2) in Fin 4, the midpoint mass-squared numerator equals eight times the explicit integer coupling table. Gravity analysts building the 4D Regge midpoint M2TT identity cite this as one atomic kernel case among 256. The proof is a single kernel decide on two fully concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the midpoint mass-squared numerator at $(1,3,0,2,3,2)$ equals eight times the explicit coupling value at the same sextuple: $m_2^{\mathrm{num}}(1,3,0,2,3,2)=8\,Z(1,3,0,2,3,2)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification. The local goal, stated in the module header, is to discharge $m_2^{\mathrm{num}}=8\cdot Z$ on a block of the $4^6=4096$ index sextuples by kernel decision (here chunk 7, 256 decides).
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 Fin-4 indices. The comparison table $Z$ is an explicit pattern-matched integer function on the same six indices (sample clauses give values such as $4$, $-2$, and so on).
Both sides are pure integers once the six indices are fixed, so each sextuple is an independent decidable equality.
proof idea
One-line kernel proof: by decide. After substituting the concrete indices $1,3,0,2,3,2$, both $m_2^{\mathrm{num}}$ (the fold of contributions) and $8\cdot Z$ reduce to closed integer numerals; the decidability procedure checks they coincide. No lemmas beyond the two definitions are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts the identity for every sextuple in $(\mathrm{Fin},4)^6$. Its proof is a six-fold fin_cases tree that bottoms out at atomic equalities such as this one. Without the chunk lemmas, the assemble step has nothing to close on.
In the broader Gravity analysis stack, the identity $m_2^{\mathrm{num}}=8Z$ is the algebraic core of the exact midpoint M2TT certificate in 4D Regge calculus. It sits downstream of the kernel coupling table and upstream of the assembled global statement used by later curvature and continuum-limit arguments. It does not itself touch the RS forcing chain (T0–T8), but it is infrastructure for the discrete-gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.