How can ws with |w| = |s| and w ≠ s be context-free while w#s is not?
Your proof is correct, and I was wrong. It took me a while to nail down where my confusion was, but with Yuval's help I think I got it.

Let's consider the three languages

$\qquad\begin{align*}
  &amp;L_=     &amp;\!\!\!\!\!\!\!\!\!
       &amp;= \{ xy   \mid |x| = |y|, x \neq y \}, \\
  &amp;L_{\#}  &amp;\!\!\!\!\!\!\!\!\!
       &amp;= \{ x\#y \mid  x \neq y \},\ \text{and} \\
  &amp;L_{=\#} &amp;\!\!\!\!\!\!\!\!\!
       &amp;= \{ x\#y \mid |x| = |y|, x \neq y \}.
\end{align*}$

As we have seen here, $L_=$ is context-free. The trick is, in the grammar, to generate symbols "on the right" but count them "on the left" later (or the other way around), making sure mismatching symbols appear at matching positions. The length condition is trivial since it reduces to even length.
You can construct an NPDA with a similar idea, using the stack to match the position.

$L_\#$ is also context-free. The proof is even simpler: the mismatching symbols appear the same distance away from the beginning resp. the separator. Unequal lengths can be checked separately; non-determinism "chooses" between the two options.

Now, as you show, $L_{=\#}$ is not context-free. Here is why the proofs for the other two languages break down.


In the grammar for $L_=$, if we have to generate a separator in the middle we can not "reassign" symbols from "left" to "right".
Instead of "accept if lengths unequal or mismatch" we have to "accept if lengths equal and mismatch". Non-determinism can not help us with the and!


So what it boils down to, intuitively, is that conditions of the form "$x \neq y$" and "$|x| = |y|$" are both "context-free" in the sense that they can be checked with a stack, but not using finite control. Therefore, a PDA can do one but not both.

The PDA for $L_=$ "cheats" since it does not really check these conditions for $x$ and $y$; it splits the word up in a different way. That's no longer possible if you have the separator.



Addendum: I boldly claimed that $L_= \in \mathrm{CFL} \implies L_{=\#} \in \mathrm{CFL}$ because CFL is closed against inverse homomorphism. While it's true that $f(L_{=\#}) = L_=$ with $f$ the identity except it deletes $\#$, that is not relevant. $f^{-1}(L_=) = L_\#$; nothing can be said about $L_{=\#}$.



Addendum II: Note that $L = \{ x\#y \mid |x| = |y| \}$ is trivially context-free. Hence, with $L \cap L_\# = L_{=\#}$ we have a nice example for CFL not being closed against intersection.