Appendix E.2, proof of Proposition 6, p. 52 — ζ(n; λ̲) − ζ(n; λ̄) = 2γ(λ̲ − λ̄)(2n − 1) < 0 for n > 1/2 (corrected value)

Let $\gamma>0$, let $\underline\lambda<\overline\lambda$ be two levels of interoperability, and let $n>1/2$. Then

In the proof of Proposition 6 this is applied at the dominant share $n=\overline n^1$ of an equilibrium under $\overline\lambda$, where $\zeta(\overline n^1;\overline\lambda)=0$, and shows $\zeta(\overline n^1;\underline\lambda)<0$.

Formalization Note The paper prints the difference as $4(\underline\lambda-\overline\lambda)\gamma\overline n^1$; the correct value, from the definition of $\zeta$, is $2\gamma(\underline\lambda-\overline\lambda)(2\overline n^1-1)$. Both are negative under the stated hypotheses, so the argument is unaffected. The Lean states the correct value and the sign.