I think the above constraint when the absolute value of the HW for 2 strings is less than the HD between those strings. Any thoughts on the proof, please?
Also, how do I make it a constraint if it's provable? It's not necessary that the explanation has to be in terms of HD and/or HW.
Let $x_i$ be an indicator variable that can only take the value $1$ if bit $i$ flips from $0$ to $1$. You can model that with the constraints $x_i \leq b_i$ and $x_i \leq 1 - a_i$. To ensure at least one flip occurs, you add $\sum_i x_i \geq 1$.
You can do the same with a variable $y_i$ that can only take the value $1$ if bit $i$ flips from $1$ to $0$.