\begin{lemma}[Mutual information bound]\label{mutual-w-z2}\lean{mutual_of_W_Z_two_le}\leanok  We have  $\bbI[W : Z_2] \leq 2 (m-1) k$.
\end{lemma}
\begin{proof}\uses{alternative-mutual, ent-w}
  From \Cref{alternative-mutual} we have $\bbI[W : Z_2] = \bbH[W] - \bbH[W | Z_2]$, and since $Z_2 = \sum_{j=1}^{m-1} j Q_j$ and $W = \sum_{j=1}^m Q_j$,
  \[
    \bbH[W | Z_2] \geq \bbH[W \,|\, Q_1,\dots,Q_{m-1}] = \bbH[Q_m] = \bbH[S].
  \]
  Hence, by \Cref{ent-w},
  \[
    \bbI[W : Z_2] \leq \bbH[W] - \bbH[S] \leq 2 (m-1) k,
  \]
  as claimed.
\end{proof}
/-- We have $\bbI[W : Z_2] \leq 2 (m-1) k$. -/
lemma mutual_of_W_Z_two_le : I[W : Z2] ≤ 2 * (p.m-1) * k := sorry