e_300323
plain-language theorem explainer
For the six Fin-4 indices (3,0,0,3,2,3), the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decision on concrete integers.
Claim. For indices $a=3$, $b=0$, $c=0$, $d=3$, $i=2$, $j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $\mathrm{m2Num}(3,0,0,3,2,3)=8\cdot\mathrm{explicitZ}(3,0,0,3,2,3)$.
background
In the 4D Regge exact-midpoint analysis, the numerator of the discrete mass-squared (or TT) identity is assembled by folding a fixed coupling list: each term contributes an integer depending on six face/edge indices in $\mathrm{Fin},4$. That fold is m2Num. Parallel to it sits explicitZ, a sparse pattern-matched integer table on the same six indices (typical nonzero values $\pm2,\pm4$).
The module is chunk 12 of a 256-way case split: every concrete sextuple is certified separately so the global identity can be reassembled by exhaustive fin_cases. The local claim is only the single sextuple $(3,0,0,3,2,3)$.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values (the fold of couplingZList versus the pattern match in explicitZ), so the equality is a decidable integer comparison discharged by the kernel with no lemmas.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states the identity for all $a,b,c,d,i,j:\mathrm{Fin},4$ and proves it by six nested fin_cases, each leaf a chunk decide such as this one. That global identity is the algebraic core of the Regge exact-midpoint M2/TT certificate in 4D gravity analysis inside the monolith. It does not itself invoke the RS forcing chain (T5–T8) or the J-cost; it is pure discrete-geometry bookkeeping needed before continuum or phenomenological gravity claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.