e_011111
plain-language theorem explainer
For the six Fin-4 indices (0,1,1,1,1,1), the discrete midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the 4D Regge exact-midpoint M2TT identity cite this as one of the 256 kernel cases. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=0$, $b=1$, $c=1$, $d=1$, $i=1$, $j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $\mathrm{m2Num}(0,1,1,1,1,1)=8\cdot\mathrm{explicitZ}(0,1,1,1,1,1)$.
background
This module is chunk 1 of a 256-case kernel certification that the discrete midpoint numerator equals eight times a closed-form integer table in four dimensions. The ambient setting is the Regge exact-midpoint analysis of the M2TT identity for 4D gravity.
The numerator m2Num is defined by folding a fixed coupling list: it sums contrib t a b c d i j over every term t in couplingZList, yielding an integer for each sextuple of Fin 4 indices. The comparison table explicitZ is a pattern-matched integer function on the same six indices (e.g. returning 4, -2, or other small constants on the listed patterns, and implicitly 0 off-pattern).
The local claim is one concrete evaluation of the identity m2Num = 8 · explicitZ at the index tuple (0,1,1,1,1,1).
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed, so the decision procedure discharges equality without lemmas or case splits inside this declaration.
why it matters
Parent theorem m2Num_eq_eight_explicitZ asserts the identity for every sextuple in Fin 4, proved by exhaustive fin_cases on all six indices. Each leaf of that case tree is one of these chunk theorems; this declaration supplies the leaf for (0,1,1,1,1,1).
In the Recognition gravity stack, the certified numerator identity is infrastructure for the exact midpoint form of the 4D Regge M2TT relation. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it hardens the discrete geometric side that those continuum limits sit on. Closing all 256 decides removes scaffolding from the assemble step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.