Reference · Signed rationals

rainbow.math.rational.signed.convex-optimality

Signed rationalssrc/rainbow/math/rational/signed/convex_optimality.clj0 definitions, 3 theorems

First-order optimality for convex objectives over signed rationals. A convex objective `f` admits, at a candidate point `x0`, a supporting linear certificate `linear` (the subgradient form `x |-> <g0, x - x0>`) with f x0 + linear x <= f x for every feasible x. The variational inequality at `x0` says that certificate never points downhill inside the feasible set: 0 <= linear x for every feasible x. Together these give global optimality of `x0` -- no local reasoning, no descent argument, no derivative calculus: f x0 = f x0 + 0 <= f x0 + linear x <= f x. This is the reason convex programs have no spurious local minima, and it is the soundness core of every optimality certificate a solver can emit. The linear certificate is kept abstract as a function, so no signed multiplication or inner product is postulated; instantiating `linear` at an inner product recovers the textbook statement. Also proved: convex certificates add (so the certificate for a sum of convex objectives is the sum of the certificates), and the sum of two certified stationary objectives is globally minimized at the shared point. Native and axiom-free; chains the D63 signed order toolkit through signed limit uniqueness (for signed/add-zero-right) and signed order monotonicity.

Depends onmath.rational.signed.limit-uniquenessmath.rational.signed.order-monotone

optimization/signed-first-order-global-minimum :
  (f linear : ℚ → ℚ) (x0 : ℚ) (feasible : ℚ → Prop)
  (certificate : ∀ (x : ℚ), ∀ (member : feasible x), f x0 + linear x ≤ f x)
  (variational : ∀ (x : ℚ), ∀ (member : feasible x), 0 ≤ linear x)
  (x : ℚ) (member : feasible x)
  → f x0 ≤ f x

optimization/signed-convex-certificate-sum :
  (f g lf lg : ℚ → ℚ) (x0 : ℚ) (feasible : ℚ → Prop)
  (f-certificate : ∀ (x : ℚ), ∀ (member : feasible x), f x0 + lf x ≤ f x)
  (g-certificate : ∀ (x : ℚ), ∀ (member : feasible x), g x0 + lg x ≤ g x)
  (x : ℚ) (member : feasible x)
  → f x0 + g x0 + (lf x + lg x) ≤ f x + g x

optimization/signed-convex-sum-global-minimum :
  (f g lf lg : ℚ → ℚ) (x0 : ℚ) (feasible : ℚ → Prop)
  (f-certificate : ∀ (x : ℚ), ∀ (member : feasible x), f x0 + lf x ≤ f x)
  (g-certificate : ∀ (x : ℚ), ∀ (member : feasible x), g x0 + lg x ≤ g x)
  (f-variational : ∀ (x : ℚ), ∀ (member : feasible x), 0 ≤ lf x)
  (g-variational : ∀ (x : ℚ), ∀ (member : feasible x), 0 ≤ lg x)
  (x : ℚ) (member : feasible x)
  → f x0 + g x0 ≤ f x + g x