your code is way to messy to see the interesting thing
Binary product x*y is linearized by replacing the product with new binary w and [w <= [x y], w >= x + y -1]
If y is continuous, you can derive the big-M model using [implies(x==1, w==y) + implies(x==0,w==0)]
If you are lazy, you can use the command binmodel.