The self-scaled two-update direction is a descent direction

Proved

ShannoCG.SCONB.sconbDirection_descent

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

bfgsconjugate-gradientp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1quasi-newton

Let $p_t, y_t, p_k, y_k, g_{k+1} \in \mathbb R^n$ with $p_t'y_t > 0$ , $p_k'y_k > 0$ and $g_{k+1} \ne 0$ , and let $d_{k+1} = -\hat H_{k+1} g_{k+1}$ be the self-scaled two-update direction ( $\hat H_k$ from (37), $\hat H_{k+1}$ its BFGS update (32) with $(p_k, y_k)$ ). Then $d_{k+1}$ is a descent direction:

g_{k+1}'\, d_{k+1} < 0.

No line-search exactness and no quadratic structure is required: the curvature condition $p'y > 0$ on each of the two updates suffices. This is why the method can be used with inexact line searches.

Formalization Note The paper's condition " $p_k'y_k > 0$ " is imposed on every update, so it is assumed for both pairs $(p_t, y_t)$ and $(p_k, y_k)$ . "Descent direction" is read as $g_{k+1}'d_{k+1} < 0$ , which needs $g_{k+1} \ne 0$ .

Preamble

import Mathlib
import Definitions.Def_ShannoCG_SCONB_sconbDirection

open Matrix

Formal statement

namespace ShannoCG.SCONB

/-- Shanno, *Conjugate Gradient Methods with Inexact Searches*, Math. Oper. Res. 3(3) (1978), §IV, p. 250 (PDF 7), the paragraph after (39): as the method uses two sequential
quasi-Newton updates, `p_k'y_k > 0` is sufficient to ensure that the search direction `d_{k+1}` is
always a descent direction. Stated here for the self-scaled algorithm (34), (38), (39), i.e.
`d_{k+1} = −Ĥ_{k+1} g_{k+1}` with `Ĥ_k` from (37) and `Ĥ_{k+1}` from (32).

**Formalization Note.** "`p_k'y_k > 0`" is the paper's condition on every update, so it is assumed
for both pairs `(p_t, y_t)` and `(p_k, y_k)`. "Descent direction" is `g_{k+1}' d_{k+1} < 0`, which
requires `g_{k+1} ≠ 0`. Generic vectors; no quadratic. -/
theorem sconbDirection_descent {n : ℕ} (pt yt pk yk g : Fin n → ℝ) (hpyt : 0 < pt ⬝ᵥ yt)
    (hpyk : 0 < pk ⬝ᵥ yk) (hg : g ≠ 0) :
    g ⬝ᵥ sconbDirection pt yt pk yk g < 0 := by sorry

end ShannoCG.SCONB

Source

Shanno, Conjugate Gradient Methods with Inexact Searches, Math. Oper. Res. 3(3) (1978) 244–256, DOI 10.1287/moor.3.3.244, p. 250 (PDF p. 7), §IV, the paragraph after eq. (39) (algorithm (34), (38), (39))

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph