Reference · Signed rationals

rainbow.math.rational.signed.big-m

Signed rationalssrc/rainbow/math/rational/signed/big_m.clj0 definitions, 2 theorems

Soundness of the indicator ("big-M") reformulation. A contract model says "this activity may only run if we have committed to it". An execution model cannot say that; it says x <= u * z, z in {0, 1}, where `u` is a bound the modeller believes the activity can never exceed. That substitution is the single most common place a linear model stops meaning what the business said, and it fails in two opposite directions: TOO TIGHT -- the row quietly forbids something the contract allowed, so the solver returns a worse plan than the business could have run and nobody can tell, because the model is still feasible; NOT BINDING -- the row fails to force the activity off, so the plan violates the commitment it was supposed to encode. The two theorems here are exactly those two directions: optimization/big-m-row-inactive : x <= u -> x <= u * 1 committing to the activity cannot cut off anything the bound already allowed, so the encoding is not too tight; optimization/big-m-forces-zero : x <= u * z -> z ~ 0 -> x <= 0 declining the activity does force the quantity to zero, so the encoding binds. Both are stated over signed rationals, so `u` may be negative and `z` is an ordinary value rather than a special-cased flag. Neither theorem assumes `u` is a VALID bound -- that is a modelling claim about the business, and it stays the modeller's to make. What is proved is that GIVEN the bound, the row means what the contract said. Native and axiom-free on D63.

Depends onmath.rational.signed.multiply-ring

optimization/big-m-row-inactive :
  (x u : ℚ)
  (bounded : x ≤ u)
  → x ≤ u · 1

optimization/big-m-forces-zero :
  (x u z : ℚ)
  (indicated : x ≤ u · z)
  (declined : z = 0)
  → x ≤ 0