Reference · Signed rationals

rainbow.math.rational.signed.multiply-order

Signed rationalssrc/rainbow/math/rational/signed/multiply_order.clj1 definitions, 8 theorems

The sign rules for signed-rational multiplication. Until now the signed layer had no order lemma about `signed/multiply` at all: the order toolkit was purely additive. The obstruction is real -- a signed product mixes the four component products positive (a*b) = Pa*Pb + Na*Nb, negative (a*b) = Pa*Nb + Na*Pb and no amount of termwise monotonicity relates those two sums, because moving one factor up moves one summand up and the other down. The two-point rearrangement inequality is exactly the missing fact, and once it is available each sign rule is a single instantiation: nonneg a, nonneg b => nonneg (a*b) [n,p,q,m := Na,Pa,Nb,Pb] nonneg a, nonpos b => nonpos (a*b) [n,p,q,m := Na,Pa,Pb,Nb] nonpos a, nonpos b => nonneg (a*b) [n,p,q,m := Pa,Na,Pb,Nb] `signed/nonnegative v` is already the codebase's zero-free predicate `negative v <= positive v`; this module adds the mirrored `signed/nonpositive` and four bridges identifying both with the order comparisons against `signed/zero`, so the sign rules can be used wherever the Lagrangian and optimality modules speak of `0 <= x` and `x <= 0`. This is what a concrete Lagrangian penalty needs: a nonnegative multiplier times a satisfied (nonpositive) constraint is nonpositive. Native and axiom-free; chains signed multiplication and the nnrat rearrangement toolkit on D63. The two additive-identity equivalences are rebuilt here as local proof terms rather than chained from rainbow.math.rational.nnrat.identities, because that module and rainbow.math.rational.nnrat.distributive (which the rearrangement toolkit needs) both declare `nnrat/multiply-one-left`, and chaining two providers of one alias is a kernel alias conflict.

Depends onmath.rational.signed.multiplymath.rational.nnrat.order-difference

signed/nonpositive :
  (x₁ : ℚ)
  → Prop

signed/multiply-nonnegative :
  (a b : ℚ) (ha : signed/nonnegative a) (hb : signed/nonnegative b)
  → signed/nonnegative (a · b)

signed/multiply-nonnegative-nonpositive :
  (a b : ℚ) (ha : signed/nonnegative a) (hb : signed/nonpositive b)
  → signed/nonpositive (a · b)

signed/multiply-nonpositive :
  (a b : ℚ) (ha : signed/nonpositive a) (hb : signed/nonpositive b)
  → signed/nonnegative (a · b)

signed/at-most-zero-of-nonpositive :
  (x : ℚ) (hx : signed/nonpositive x)
  → x ≤ 0

signed/nonpositive-of-at-most-zero :
  (x : ℚ)
  (hx : x ≤ 0)
  → signed/nonpositive x

signed/zero-at-most-of-nonnegative :
  (x : ℚ) (hx : signed/nonnegative x)
  → 0 ≤ x

signed/nonnegative-of-zero-at-most :
  (x : ℚ)
  (hx : 0 ≤ x)
  → signed/nonnegative x

optimization/signed-multiplier-penalty-nonpositive :
  (lambda g : ℚ)
  (hlambda : 0 ≤ lambda)
  (hg : g ≤ 0)
  → lambda · g ≤ 0