e_211121
plain-language theorem explainer
For the six Fin-4 index tuple (2,1,1,1,2,1), the folded numerator m2Num equals eight times the closed-form integer table explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2,b=1,c=1,d=1,i=2,j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the numerator of the discrete M2TT kernel is assembled by folding a fixed coupling list: m2Num sums contrib terms over couplingZList for six Fin-4 indices. The companion table explicitZ is a sparse pattern-matched integer function on the same six indices (typical nonzero values are $\pm 2,\pm 4$).
The module is chunk 9 of a 256-cell kernel certification that every index sextuple satisfies m2Num = 8 · explicitZ. The local setting is pure integer arithmetic on Fin 4, with no continuum limit or metric hypotheses yet in play.
Upstream, m2Num and explicitZ are defined in the KernelCert module; this chunk only evaluates one concrete cell of that identity.
proof idea
One-line kernel proof: by decide. Lean reduces both sides of the equality on the fixed Fin-4 sextuple (2,1,1,1,2,1) to concrete integers and checks equality by computation. No lemmas beyond the definitions of m2Num and explicitZ are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ quantifies over all six Fin-4 indices and discharges the universal claim by fin_cases, invoking one cell theorem per sextuple. This declaration is cell (2,1,1,1,2,1) in that case tree (chunk 9 of the 256 decides).
In the broader Gravity analysis, the identity m2Num = 8 · explicitZ collapses the folded coupling sum to a closed integer table, which is the algebraic backbone of the exact midpoint M2TT kernel in 4D Regge calculus. It does not itself touch the T0–T8 forcing chain or the phi-ladder mass formula; 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.