Reference · Signed rationals

rainbow.math.rational.signed.lp-free-price

Signed rationalssrc/rainbow/math/rational/signed/lp_free_price.clj0 definitions, 4 theorems

Equality dual-price splitting over signed rationals. A certified p ~ pplus - pminus preserves every coefficient contribution. Component witnesses are nonnegative, but need not be the host max-based split for a noncanonical Grothendieck representative. No host execution claim.

Depends onmath.rational.signed.lp-objective-negatemath.rational.signed.distributive

signed/lp-free-price-split-contribution :
  (v p pp pm : ℚ)
  (same : p = pp - pm)
  → v · p = v · pp + signed/negate v · pm

signed/lp-price-components-reconstruct :
  (p : ℚ)
  → p = signed/from-nnrat (signed/positive p) - signed/from-nnrat (signed/negative p)

signed/lp-price-components-nonnegative :
  (p : ℚ)
  → proposition/conjunction (0 ≤ signed/from-nnrat (signed/positive p)) (0 ≤ signed/from-nnrat (signed/negative p))

signed/lp-price-components-contribution :
  (v p : ℚ)
  → v · p = v · signed/from-nnrat (signed/positive p) + signed/negate v · signed/from-nnrat (signed/negative p)