Skip to main content

gam_solve/rho_optimizer/
kl_certificate.rs

1//! KL rate-certificate module (#2337 §9 step 7).
2//!
3//! This module observes the outer smoothing-parameter loop's stream of
4//! *accepted-step objective decreases* and answers one question with a
5//! certificate rather than a heuristic: **will this loop reach its target
6//! tolerance within the remaining iteration budget, and if not, is that
7//! because it is converging too slowly or because it is defective?**
8//!
9//! The distinction matters. A loop that is *provably converging but slow*
10//! deserves a `RateCertified` refusal that names the forecast — the caller
11//! can raise the budget. A loop whose accepted steps contradict the solver's
12//! own monotone-descent contract is *defective*: no budget will save it, and
13//! we say so (`KlInconsistent`) from an **exact theorem**, never from a noisy
14//! rate fit.
15//!
16//! # Why a rate can be *named*, not merely assumed
17//!
18//! The outer criterion this engine certifies (the REML/Laplace objective on
19//! the certification tube) is real-analytic there — it is `C^ω`, see #2337
20//! Thm 5.3. A real-analytic function satisfies the **Łojasiewicz gradient
21//! inequality**
22//!
23//! ```text
24//!     ‖∇V(x)‖ ≥ c · |V(x) − V*|^θ ,   θ ∈ [1/2, 1),
25//! ```
26//!
27//! on a neighborhood of any critical point `x*`, with some exponent `θ` and
28//! constant `c > 0`. Existence of `θ` is therefore *guaranteed*; this module
29//! only *names* it from the observed decreases. It never assumes convergence
30//! — a bad fit yields [`LoopVerdict::InsufficientData`], and a contract
31//! violation yields [`LoopVerdict::KlInconsistent`] from a defect theorem.
32//!
33//! # From the Łojasiewicz exponent to the observable decrease slope
34//!
35//! Let `e_k = V_k − V*` be the optimality gap (`e_k → 0`, monotone
36//! decreasing under a descent method) and `d_k = e_k − e_{k+1} = V_k − V_{k+1}`
37//! the accepted-step decrease. Assume **sufficient decrease**
38//!
39//! ```text
40//!     d_k ≥ a · ‖∇V_k‖²                                          (SD)
41//! ```
42//!
43//! (Armijo / trust-region / MM all provide (SD) with some `a > 0`).
44//! Combining (SD) with Łojasiewicz gives the scalar recurrence
45//!
46//! ```text
47//!     e_k − e_{k+1} ≥ a c² · e_k^{2θ}.                            (R)
48//! ```
49//!
50//! **Case θ = 1/2.** (R) reads `e_k − e_{k+1} ≥ a c² e_k`, i.e.
51//! `e_{k+1} ≤ (1 − a c²) e_k` — *linear* (geometric) convergence,
52//! `e_k ≍ r^k` with `r = 1 − a c² ∈ (0,1)`. Since
53//! `d_k = e_k(1 − e_{k+1}/e_k) ≍ e_k`, the *decreases are geometric too*:
54//! `d_k ≍ r^k`. This is the `Geometric` model.
55//!
56//! **Case θ ∈ (1/2, 1).** Treat (R) as the continuum ODE
57//! `ė = −C e^{2θ}` with `2θ > 1`. Then
58//! `d/dk (e^{1−2θ}) = (1−2θ) e^{−2θ} ė = C(2θ−1) > 0`, so
59//! `e_k^{1−2θ} ≍ C(2θ−1) k`, giving the sublinear gap
60//!
61//! ```text
62//!     e_k ≍ k^{−1/(2θ−1)}.
63//! ```
64//!
65//! Differentiating, `d_k ≍ −de/dk ≍ k^{−(1/(2θ−1) + 1)} = k^{−s}` with the
66//! **observable decrease slope**
67//!
68//! ```text
69//!     s = 1/(2θ−1) + 1 = 2θ/(2θ−1).                              (S)
70//! ```
71//!
72//! Note the valid range: for `θ ∈ (1/2, 1)`, (S) maps to `s ∈ (2, ∞)`
73//! (`θ=3/4 ↦ s=3`, `θ=5/6 ↦ s=2.5`, `θ→1 ↦ s→2`, `θ→1/2⁺ ↦ s→∞`).
74//! The gap exponent `p = 1/(2θ−1) = s − 1 ∈ (1, ∞)`, so the gap is always
75//! summable — the telescoped forecast below is well-defined.
76//!
77//! # Sign convention for θ̂ — reconciled explicitly
78//!
79//! We fit `log d_k` linearly against `log k` by least squares and read off
80//! the **raw slope** `ŝ_raw`. Because `d_k` *decreases*, `ŝ_raw < 0`, and its
81//! magnitude is the `s` of (S): `s = −ŝ_raw`. Inverting (S) for `θ`:
82//!
83//! ```text
84//!     s = 2θ/(2θ−1)  ⟹  s(2θ−1) = 2θ  ⟹  2θ(s−1) = s
85//!                    ⟹  θ = s / (2s − 2).                        (I)
86//! ```
87//!
88//! Substituting the *raw* (negative) slope `s = −ŝ_raw` into (I):
89//!
90//! ```text
91//!     θ = (−ŝ_raw) / (2(−ŝ_raw) − 2)
92//!       = (−ŝ_raw) / (−2 ŝ_raw − 2)
93//!       = ŝ_raw / (2 ŝ_raw + 2).                                 (I')
94//! ```
95//!
96//! So **`θ̂ = ŝ_raw / (2 ŝ_raw + 2)`** with `ŝ_raw` the raw (negative)
97//! log-log slope — this is exactly the parametrization the #2337 theory doc
98//! records as `θ̂ = ŝ/(2ŝ+2)`. We therefore store the **raw negative slope**
99//! in [`RateModel::Power::exponent_s`] and compute `kl_theta` via (I').
100//!
101//! Sanity: `ŝ_raw = −3` (i.e. `d_k ≍ k^{−3}`, the `f(x)=x⁴` case, `θ=3/4`)
102//! gives `θ̂ = −3/(−6+2) = 0.75`. `ŝ_raw = −2.5` (the `f(x)=x⁶` case,
103//! `θ=5/6`) gives `θ̂ = −2.5/(−5+2) = 0.8333`. ✓
104//!
105//! # Forecasts
106//!
107//! Given a current gap bound `e` and target `tol` (`0 < tol < e`):
108//!
109//! * **Geometric** (`e_k ≍ e·r^n`): `e·r^N ≤ tol ⟺ N ≥ log(tol/e)/log(r)`,
110//!   so `N̂ = log(tol/e) / log(r)` (both logs negative, `N̂ > 0`).
111//!
112//! * **Power** (`e_k ≍ C k^{−p}`, `p = s − 1`, `s = −exponent_s`): with the
113//!   loop currently at iteration `k_now`, `e = C k_now^{−p}` and we need
114//!   `C k_target^{−p} ≤ tol`. Dividing, `(k_target/k_now)^{−p} = tol/e`, so
115//!   `k_target = k_now (e/tol)^{1/p}` and the *additional* iterations are
116//!
117//!   ```text
118//!       N̂ = k_target − k_now = k_now · ((e/tol)^{1/p} − 1),
119//!       p = s − 1 = (−exponent_s) − 1.                           (F)
120//!   ```
121//!
122//!   Convention reconciliation: the #2337 task sketch wrote the power
123//!   forecast exponent as `1/(s_pos+1)`. That does not survive the
124//!   telescoping derivation — the gap exponent is `p = s − 1` (the gap is one
125//!   power *shallower* than the decreases `d_k ≍ k^{−s}`, because
126//!   `d_k = −de/dk`), so the correct forecast exponent is `1/(s−1)`, which is
127//!   what (F) uses. We flag this as the derivation-correct form.
128//!
129//! `Grant` iff `N̂ ≤ budget`; otherwise `RateCertified` (a provable-but-slow
130//! refusal carrying the forecast). A non-convergent fit (geometric `r ≥ 1`,
131//! or power `p ≤ 0`) is treated as an *uninformative* fit —
132//! [`LoopVerdict::InsufficientData`], never a defect claim.
133//!
134//! # Defect theorems (exact — not fits)
135//!
136//! See [`monotonicity_defect`] and [`energy_budget_defect`]. These are the
137//! *only* sources of [`LoopVerdict::KlInconsistent`]: they are proofs, valid
138//! independent of any rate model.
139
140use std::collections::VecDeque;
141
142use gam_linalg::utils::KahanSum;
143
144/// Default ring-buffer capacity `W` for [`DecreaseWindow`].
145///
146/// Chosen to hold enough recent accepted steps for a stable two-parameter
147/// log/log-log least-squares fit while staying local to the current basin.
148pub const DEFAULT_WINDOW_CAPACITY: usize = 24;
149
150/// Minimum number of positive-decrease points required before a rate fit is
151/// attempted. Two points fit any line exactly (zero residual for *both*
152/// models — an uninformative tie); three is the smallest count at which the
153/// residual-based model selection carries signal.
154const MIN_FIT_POINTS: usize = 3;
155
156/// Guard for the `2ŝ_raw + 2` denominator in the θ̂ inversion (I'). In the
157/// valid regime `ŝ_raw < −2` so the denominator is `< −2`; a value near zero
158/// means the fit landed outside the certifiable band and the power model is
159/// rejected as uninformative.
160const POWER_THETA_MIN_DENOM: f64 = 1.0e-9;
161
162/// Relative backward-error band used by [`assess`] when it screens the window
163/// for a monotonicity defect. An accepted-step *increase* below
164/// `MONOTONICITY_ROUNDING_BAND_REL · max|d_k|` is attributed to floating-point
165/// rounding in the objective evaluation, not to a genuine contract violation.
166/// Callers wanting a bespoke band call [`monotonicity_defect`] directly.
167const MONOTONICITY_ROUNDING_BAND_REL: f64 = 4.0 * f64::EPSILON;
168
169/// One accepted outer step's contribution to the decrease record.
170#[derive(Clone, Copy, Debug, PartialEq)]
171pub struct DecreaseEntry {
172    /// Outer iteration index `k` at which this step was accepted. Must be
173    /// `≥ 1` to participate in the power (`log k`) fit.
174    pub iter_index: u64,
175    /// Signed objective decrease `d_k = V_k − V_{k+1}`. Positive on genuine
176    /// descent; a non-positive value records an accepted-step *increase* and
177    /// is the raw material of the monotonicity defect theorem.
178    pub decrease: f64,
179    /// Squared step norm `‖x_{k+1} − x_k‖²` for this accepted step. Feeds the
180    /// energy-budget accumulator.
181    pub step_norm_sq: f64,
182}
183
184/// A fixed-capacity deterministic ring buffer of accepted-step decreases.
185///
186/// The ring holds the most recent `W` entries (for the *local* rate fit),
187/// while two compensated (Kahan) accumulators track the *lifetime* totals of
188/// decrease and squared step norm — these never evict, so they remain valid
189/// inputs to the telescoped energy budget over the whole run.
190///
191/// Determinism: `VecDeque` preserves insertion order; eviction is strictly
192/// FIFO; the Kahan accumulators are updated in push order. No randomness, no
193/// unordered iteration.
194#[derive(Clone, Debug)]
195pub struct DecreaseWindow {
196    capacity: usize,
197    ring: VecDeque<DecreaseEntry>,
198    total_decrease: KahanSum,
199    total_step_norm_sq: KahanSum,
200    observed_count: u64,
201}
202
203impl Default for DecreaseWindow {
204    fn default() -> Self {
205        Self::with_capacity(DEFAULT_WINDOW_CAPACITY)
206    }
207}
208
209impl DecreaseWindow {
210    /// A window with the [`DEFAULT_WINDOW_CAPACITY`].
211    pub fn new() -> Self {
212        Self::default()
213    }
214
215    /// A window with an explicit ring capacity `W`. A capacity of zero is
216    /// promoted to one so the ring can always hold the most recent step.
217    pub fn with_capacity(capacity: usize) -> Self {
218        let capacity = capacity.max(1);
219        Self {
220            capacity,
221            ring: VecDeque::with_capacity(capacity),
222            total_decrease: KahanSum::default(),
223            total_step_norm_sq: KahanSum::default(),
224            observed_count: 0,
225        }
226    }
227
228    /// Record one accepted step. `decrease` is signed (`V_k − V_{k+1}`);
229    /// `step_norm_sq` is `‖x_{k+1} − x_k‖² ≥ 0`. The lifetime accumulators are
230    /// updated first (they see every step), then the ring evicts its oldest
231    /// entry if full.
232    pub fn push(&mut self, iter_index: u64, decrease: f64, step_norm_sq: f64) {
233        self.total_decrease.add(decrease);
234        self.total_step_norm_sq.add(step_norm_sq);
235        self.observed_count += 1;
236        if self.ring.len() == self.capacity {
237            self.ring.pop_front();
238        }
239        self.ring.push_back(DecreaseEntry {
240            iter_index,
241            decrease,
242            step_norm_sq,
243        });
244    }
245
246    /// The ring's capacity `W`.
247    pub fn capacity(&self) -> usize {
248        self.capacity
249    }
250
251    /// Number of entries currently retained in the ring (`≤ W`).
252    pub fn len(&self) -> usize {
253        self.ring.len()
254    }
255
256    /// Whether the ring is empty.
257    pub fn is_empty(&self) -> bool {
258        self.ring.is_empty()
259    }
260
261    /// The retained entries, oldest to newest.
262    pub fn entries(&self) -> impl Iterator<Item = &DecreaseEntry> {
263        self.ring.iter()
264    }
265
266    /// Lifetime total decrease `Σ_k d_k` (compensated).
267    pub fn total_decrease(&self) -> f64 {
268        self.total_decrease.sum()
269    }
270
271    /// Lifetime total squared step norm `Σ_k ‖x_{k+1} − x_k‖²` (compensated).
272    pub fn total_step_norm_sq(&self) -> f64 {
273        self.total_step_norm_sq.sum()
274    }
275
276    /// Total number of accepted steps ever recorded (includes evicted ones).
277    pub fn observed_count(&self) -> u64 {
278        self.observed_count
279    }
280
281    /// The most recent iteration index, or `None` if empty.
282    fn latest_iter(&self) -> Option<u64> {
283        self.ring.back().map(|e| e.iter_index)
284    }
285
286    /// Largest `|d_k|` currently retained (for the rounding-band scale).
287    fn max_abs_decrease(&self) -> f64 {
288        self.ring
289            .iter()
290            .map(|e| e.decrease.abs())
291            .fold(0.0_f64, f64::max)
292    }
293}
294
295/// A fitted decrease-rate model with its log-space residual sum of squares.
296#[derive(Clone, Copy, Debug, PartialEq)]
297pub enum RateModel {
298    /// Geometric decreases `d_k ≍ ratio^k` (Łojasiewicz exponent `θ = 1/2`,
299    /// linear convergence of the gap). `ratio = exp(slope of log d_k vs k)`.
300    Geometric {
301        /// Geometric ratio `r = exp(m)`, `m` = slope of `log d_k` against `k`.
302        ratio: f64,
303        /// Residual sum of squares of the `log d_k`-vs-`k` fit.
304        resid: f64,
305    },
306    /// Power-law decreases `d_k ≍ k^{exponent_s}` (Łojasiewicz exponent
307    /// `θ ∈ (1/2, 1)`, sublinear convergence). `exponent_s` is the **raw
308    /// (negative) log-log slope** `ŝ_raw`; `kl_theta = ŝ_raw/(2ŝ_raw+2)` per
309    /// (I') in the module docs.
310    Power {
311        /// Raw log-log slope `ŝ_raw = slope of log d_k vs log k` (negative on
312        /// a converging loop; magnitude `s = −exponent_s ∈ (2, ∞)`).
313        exponent_s: f64,
314        /// Recovered Łojasiewicz exponent `θ̂ = ŝ_raw / (2ŝ_raw + 2)`.
315        kl_theta: f64,
316        /// Residual sum of squares of the `log d_k`-vs-`log k` fit.
317        resid: f64,
318    },
319}
320
321impl RateModel {
322    /// The log-space residual sum of squares of this fit (used for model
323    /// selection).
324    pub fn resid(&self) -> f64 {
325        match self {
326            RateModel::Geometric { resid, .. } => *resid,
327            RateModel::Power { resid, .. } => *resid,
328        }
329    }
330}
331
332/// The certificate/refusal returned by [`assess`].
333#[derive(Clone, Debug, PartialEq)]
334pub enum LoopVerdict {
335    /// The winning rate model forecasts reaching `tol` within budget.
336    Grant {
337        /// Forecast additional iterations `N̂` to reach `tol`.
338        forecast_iters: f64,
339        /// The winning rate model.
340        model: RateModel,
341    },
342    /// Provably converging (a valid rate was named) but the forecast exceeds
343    /// the budget — a refusal that carries the evidence so the caller can
344    /// raise the budget rather than abandon the loop.
345    RateCertified {
346        /// Forecast additional iterations `N̂` to reach `tol`.
347        forecast_iters: f64,
348        /// The winning rate model.
349        model: RateModel,
350    },
351    /// A defect theorem fired: the accepted-step stream contradicts the
352    /// loop's own descent contract. Never produced by a mere bad fit.
353    KlInconsistent {
354        /// Human-readable proof-of-defect explanation.
355        reason: String,
356    },
357    /// Not enough (or too degenerate) data to name a rate. Includes the case
358    /// of a fit that names a *non-convergent* model.
359    InsufficientData,
360}
361
362/// A least-squares line fit `y ≈ intercept + slope·x` with its residual sum
363/// of squares. All sums use compensated (Kahan) accumulation in fixed index
364/// order for determinism.
365struct LineFit {
366    slope: f64,
367    rss: f64,
368    // intercept retained implicitly via the residual computation; not exposed.
369}
370
371/// Deterministic ordinary-least-squares line fit. Returns `None` when the
372/// regressor has zero spread (`Σ(x−x̄)² = 0`) or fewer than two points.
373fn least_squares_line(xs: &[f64], ys: &[f64]) -> Option<LineFit> {
374    let n = xs.len();
375    if n < 2 || ys.len() != n {
376        return None;
377    }
378    let nf = n as f64;
379    let mut sum_x = KahanSum::default();
380    let mut sum_y = KahanSum::default();
381    for i in 0..n {
382        sum_x.add(xs[i]);
383        sum_y.add(ys[i]);
384    }
385    let mean_x = sum_x.sum() / nf;
386    let mean_y = sum_y.sum() / nf;
387    let mut sxx = KahanSum::default();
388    let mut sxy = KahanSum::default();
389    for i in 0..n {
390        let dx = xs[i] - mean_x;
391        sxx.add(dx * dx);
392        sxy.add(dx * (ys[i] - mean_y));
393    }
394    let sxx = sxx.sum();
395    if !(sxx > 0.0) {
396        return None;
397    }
398    let slope = sxy.sum() / sxx;
399    let intercept = mean_y - slope * mean_x;
400    let mut rss = KahanSum::default();
401    for i in 0..n {
402        let pred = intercept + slope * xs[i];
403        let r = ys[i] - pred;
404        rss.add(r * r);
405    }
406    Some(LineFit {
407        slope,
408        rss: rss.sum(),
409    })
410}
411
412/// Fit both the geometric and power decrease models to the window and select
413/// the one with the smaller log-space residual.
414///
415/// * Geometric: least squares of `log d_k` against `k`; `ratio = exp(slope)`.
416/// * Power: least squares of `log d_k` against `log k`; `exponent_s = slope`
417///   (raw, negative) and `kl_theta = exponent_s/(2·exponent_s+2)` per (I').
418///
419/// Only entries with `d_k > 0` and `iter_index ≥ 1` participate (both are
420/// required for the logarithms). Fewer than [`MIN_FIT_POINTS`] such entries
421/// ⇒ `None`.
422///
423/// **Tie-break (determinism).** When both models fit and their residuals are
424/// equal (`resid_power == resid_geom`, including the exact-fit degenerate
425/// case), we select **Geometric**. Geometric is the `θ = 1/2` boundary model
426/// — the fastest rate consistent with Łojasiewicz — so breaking ties toward
427/// it is the conservative (least-optimistic-θ, but fastest-forecast) choice
428/// and is fully determined by the strict `<` comparison below.
429pub fn fit_rate(window: &DecreaseWindow) -> Option<RateModel> {
430    let mut ks: Vec<f64> = Vec::new();
431    let mut ln_k: Vec<f64> = Vec::new();
432    let mut ln_d: Vec<f64> = Vec::new();
433    for e in window.entries() {
434        if e.decrease > 0.0 && e.iter_index >= 1 {
435            let k = e.iter_index as f64;
436            ks.push(k);
437            ln_k.push(k.ln());
438            ln_d.push(e.decrease.ln());
439        }
440    }
441    if ks.len() < MIN_FIT_POINTS {
442        return None;
443    }
444
445    let geometric = least_squares_line(&ks, &ln_d).and_then(|fit| {
446        let ratio = fit.slope.exp();
447        if ratio.is_finite() {
448            Some(RateModel::Geometric {
449                ratio,
450                resid: fit.rss,
451            })
452        } else {
453            None
454        }
455    });
456
457    let power = least_squares_line(&ln_k, &ln_d).and_then(|fit| {
458        let denom = 2.0 * fit.slope + 2.0;
459        if denom.abs() <= POWER_THETA_MIN_DENOM {
460            return None;
461        }
462        let theta = fit.slope / denom;
463        if theta.is_finite() {
464            Some(RateModel::Power {
465                exponent_s: fit.slope,
466                kl_theta: theta,
467                resid: fit.rss,
468            })
469        } else {
470            None
471        }
472    });
473
474    match (geometric, power) {
475        // Strict `<` sends ties to Geometric.
476        (Some(g), Some(p)) => Some(if p.resid() < g.resid() { p } else { g }),
477        (Some(g), None) => Some(g),
478        (None, Some(p)) => Some(p),
479        (None, None) => None,
480    }
481}
482
483/// Forecast the additional iterations `N̂` a model needs to drive the gap from
484/// `current_gap_bound` to `target_tol`, or `None` if the model is
485/// non-convergent (geometric `r ∉ (0,1)`, power gap-exponent `p ≤ 0`) or the
486/// inputs are degenerate.
487fn forecast_iters(model: &RateModel, current_gap_bound: f64, target_tol: f64, k_now: f64) -> Option<f64> {
488    if !(current_gap_bound > 0.0) || !(target_tol > 0.0) {
489        return None;
490    }
491    // Already at or below target: nothing more to do.
492    if current_gap_bound <= target_tol {
493        return Some(0.0);
494    }
495    match *model {
496        RateModel::Geometric { ratio, .. } => {
497            if !(ratio > 0.0 && ratio < 1.0) {
498                return None;
499            }
500            // N̂ = log(tol/e) / log(r); both logs negative ⇒ N̂ > 0.
501            let n = (target_tol / current_gap_bound).ln() / ratio.ln();
502            if n.is_finite() && n >= 0.0 {
503                Some(n)
504            } else {
505                None
506            }
507        }
508        RateModel::Power { exponent_s, .. } => {
509            // Gap exponent p = s − 1 with s = −exponent_s (decrease slope
510            // magnitude). Gap ≍ k^{−p}; forecast per (F).
511            let s = -exponent_s;
512            let p = s - 1.0;
513            if !(p > 0.0) || !(k_now > 0.0) {
514                return None;
515            }
516            let ratio = current_gap_bound / target_tol; // > 1 here
517            let n = k_now * (ratio.powf(1.0 / p) - 1.0);
518            if n.is_finite() && n >= 0.0 {
519                Some(n)
520            } else {
521                None
522            }
523        }
524    }
525}
526
527/// Assess the loop: certificate or refusal.
528///
529/// Order of reasoning:
530/// 1. **Defect first.** Screen the window for a monotonicity defect with the
531///    default relative rounding band; if it fires, return `KlInconsistent`
532///    (an exact proof outranks any rate forecast). Callers needing the
533///    energy-budget defect (which requires `V_0`/`V_lb`/`a`) call
534///    [`energy_budget_defect`] directly.
535/// 2. **Name the rate.** [`fit_rate`]; a `None` fit — or a fit whose model is
536///    non-convergent, so the forecast is undefined — is `InsufficientData`,
537///    *never* a defect claim.
538/// 3. **Forecast & decide.** `Grant` iff `N̂ ≤ iter_budget`, else
539///    `RateCertified` carrying the forecast.
540pub fn assess(
541    window: &DecreaseWindow,
542    current_gap_bound: f64,
543    target_tol: f64,
544    iter_budget: f64,
545) -> LoopVerdict {
546    let band = MONOTONICITY_ROUNDING_BAND_REL * window.max_abs_decrease();
547    if let Some(reason) = monotonicity_defect(window, band) {
548        return LoopVerdict::KlInconsistent { reason };
549    }
550
551    let model = match fit_rate(window) {
552        Some(m) => m,
553        None => return LoopVerdict::InsufficientData,
554    };
555
556    let k_now = match window.latest_iter() {
557        Some(k) => k as f64,
558        None => return LoopVerdict::InsufficientData,
559    };
560
561    match forecast_iters(&model, current_gap_bound, target_tol, k_now) {
562        Some(n) if n <= iter_budget => LoopVerdict::Grant {
563            forecast_iters: n,
564            model,
565        },
566        Some(n) => LoopVerdict::RateCertified {
567            forecast_iters: n,
568            model,
569        },
570        // Non-convergent model / degenerate inputs: an uninformative fit, not
571        // a defect.
572        None => LoopVerdict::InsufficientData,
573    }
574}
575
576/// **Monotonicity defect theorem.**
577///
578/// An MM / sufficient-decrease outer loop guarantees *monotone decrease*: at
579/// every accepted step `V_{k+1} ≤ V_k`, i.e. `d_k = V_k − V_{k+1} ≥ 0`. An
580/// accepted step with `d_k < 0` (the objective *rose*) beyond the objective's
581/// backward-error band `rounding_band` therefore **contradicts the loop's own
582/// contract** — a proof of defect, independent of any convergence rate.
583///
584/// Returns `Some(reason)` naming the *earliest* (lowest `iter_index`, then
585/// lowest ring position) offending step for determinism; `None` if every
586/// retained step decreases within the band.
587pub fn monotonicity_defect(window: &DecreaseWindow, rounding_band: f64) -> Option<String> {
588    let band = rounding_band.abs();
589    let mut worst: Option<&DecreaseEntry> = None;
590    for e in window.entries() {
591        if e.decrease < -band {
592            worst = match worst {
593                None => Some(e),
594                Some(prev) if e.iter_index < prev.iter_index => Some(e),
595                Some(prev) => Some(prev),
596            };
597        }
598    }
599    worst.map(|e| {
600        format!(
601            "monotonicity defect: accepted step at iter {} increased the objective by {:.6e} \
602             (d_k = {:.6e} < -band {:.6e}); an MM/sufficient-decrease loop guarantees d_k >= 0, \
603             so this contradicts the loop's descent contract",
604            e.iter_index,
605            -e.decrease,
606            e.decrease,
607            band
608        )
609    })
610}
611
612/// **Energy-budget defect theorem.**
613///
614/// Sufficient decrease in step-norm form, `d_k = V_k − V_{k+1} ≥ a·‖x_{k+1} −
615/// x_k‖²` with `a > 0` (trust-region and Armijo line searches both furnish
616/// this: the accepted decrease dominates a constant times the squared step),
617/// telescopes over `k = 0 … K−1`:
618///
619/// ```text
620///     V_0 − V_K = Σ_k d_k ≥ a · Σ_k ‖x_{k+1} − x_k‖².
621/// ```
622///
623/// Since the objective is bounded below by `V_lb ≤ V_K`,
624///
625/// ```text
626///     Σ_k ‖x_{k+1} − x_k‖² ≤ (V_0 − V_K)/a ≤ (V_0 − V_lb)/a.       (B)
627/// ```
628///
629/// The right-hand side is the **energy budget**. Observing a total squared
630/// step norm exceeding it *proves* that some accepted step violated
631/// `d_k ≥ a‖step_k‖²`, i.e. the sufficient-decrease contract is defective.
632///
633/// Returns `Some(reason)` when `total_step_norm_sq` exceeds `(V_0 − V_lb)/a`;
634/// `None` when the budget holds or when the inputs are outside the theorem's
635/// hypotheses (`a ≤ 0`, or `V_0 < V_lb`, in which case no defect is asserted).
636pub fn energy_budget_defect(
637    total_step_norm_sq: f64,
638    initial_value: f64,
639    lower_bound: f64,
640    sufficient_decrease_a: f64,
641) -> Option<String> {
642    if !(sufficient_decrease_a > 0.0) || !(initial_value >= lower_bound) {
643        // Hypotheses of (B) not met — cannot certify a defect.
644        return None;
645    }
646    let budget = (initial_value - lower_bound) / sufficient_decrease_a;
647    if total_step_norm_sq > budget {
648        Some(format!(
649            "energy-budget defect: total step energy Σ‖x_{{k+1}}−x_k‖² = {:.6e} exceeds the \
650             sufficient-decrease budget (V_0 − V_lb)/a = ({:.6e} − {:.6e})/{:.6e} = {:.6e}; by the \
651             telescoped bound this proves some accepted step violated d_k ≥ a‖step_k‖²",
652            total_step_norm_sq, initial_value, lower_bound, sufficient_decrease_a, budget
653        ))
654    } else {
655        None
656    }
657}
658
659#[cfg(test)]
660mod kl_certificate_tests {
661    use super::*;
662
663    /// Push a synthetic geometric decrease sequence `d_k = d0 · r^k` into a
664    /// fresh window over iterations `1..=n`.
665    fn geometric_window(d0: f64, r: f64, n: u64) -> DecreaseWindow {
666        let mut w = DecreaseWindow::new();
667        for k in 1..=n {
668            let d = d0 * r.powi(k as i32);
669            w.push(k, d, d); // step_norm_sq unused by these asserts
670        }
671        w
672    }
673
674    /// (a) A geometric sequence with ratio 0.994 is recovered as Geometric,
675    /// with the forecast/Grant/RateCertified behavior mirroring exp3.
676    #[test]
677    fn geometric_ratio_recovered_and_budget_decides() {
678        let r = 0.994_f64;
679        let window = geometric_window(1.0, r, 24);
680
681        let model = fit_rate(&window).expect("geometric fit");
682        match model {
683            RateModel::Geometric { ratio, .. } => {
684                assert!(
685                    (ratio - r).abs() < 1.0e-3,
686                    "recovered ratio {ratio} should be within 1e-3 of {r}"
687                );
688            }
689            other => panic!("expected Geometric, got {other:?}"),
690        }
691
692        // Forecast setup mirroring exp3: gap e=1.0, tol chosen so N̂ ≈ 599.
693        // N̂ = log(tol/e)/log(r). With r=0.994, log(r)=-6.018e-3; picking
694        // tol = exp(599·log r) gives N̂ = 599 exactly.
695        let e = 1.0_f64;
696        let n_target = 599.0_f64;
697        let tol = (n_target * r.ln()).exp(); // ≈ 2.72e-2
698
699        // Grant when the budget clears the forecast.
700        match assess(&window, e, tol, 600.0) {
701            LoopVerdict::Grant {
702                forecast_iters, ..
703            } => {
704                assert!(
705                    (forecast_iters - n_target).abs() < 1.0,
706                    "forecast {forecast_iters} should be ≈ {n_target}"
707                );
708            }
709            other => panic!("expected Grant at budget 600, got {other:?}"),
710        }
711
712        // RateCertified (provable-but-slow refusal) when the budget is below
713        // the forecast.
714        match assess(&window, e, tol, 550.0) {
715            LoopVerdict::RateCertified {
716                forecast_iters, ..
717            } => {
718                assert!(
719                    (forecast_iters - n_target).abs() < 1.0,
720                    "refusal forecast {forecast_iters} should be ≈ {n_target}"
721                );
722            }
723            other => panic!("expected RateCertified at budget 550, got {other:?}"),
724        }
725    }
726
727    /// Deterministic gradient descent on `f(x) = x^m` from `x0 = 1`.
728    /// Returns the accepted decreases `d_k = f(x_k) − f(x_{k+1})` for
729    /// `k = 0 …` alongside the iteration indices `k+1`.
730    fn power_descent_decreases(m: i32, eta: f64, steps: usize) -> Vec<(u64, f64)> {
731        let mut x = 1.0_f64;
732        let f = |x: f64| x.powi(m);
733        let grad = |x: f64| (m as f64) * x.powi(m - 1);
734        let mut out = Vec::with_capacity(steps);
735        for k in 0..steps {
736            let fx = f(x);
737            let x_next = x - eta * grad(x);
738            let fx_next = f(x_next);
739            let d = fx - fx_next;
740            out.push(((k as u64) + 1, d));
741            x = x_next;
742        }
743        out
744    }
745
746    /// Build a window from a deterministic subsample of a descent sequence:
747    /// indices `start, start+step, …` for `count` points (wide log-k leverage
748    /// deep in the asymptotic regime).
749    fn subsampled_window(seq: &[(u64, f64)], start: usize, step: usize, count: usize) -> DecreaseWindow {
750        let mut w = DecreaseWindow::with_capacity(count);
751        for j in 0..count {
752            let idx = start + j * step;
753            let (iter, d) = seq[idx];
754            w.push(iter, d, 0.0);
755        }
756        w
757    }
758
759    /// (b) Gradient descent on x⁴ (Łojasiewicz θ = 3/4). The recovered θ̂ must
760    /// land in (0.72, 0.78) and the model must be selected as Power.
761    #[test]
762    fn power_theta_recovered_x4() {
763        let seq = power_descent_decreases(4, 0.01, 3200);
764        // Subsample deep-asymptotic indices 800, 900, …, 3100 (24 points).
765        let window = subsampled_window(&seq, 799, 100, 24);
766        let model = fit_rate(&window).expect("power fit x4");
767        match model {
768            RateModel::Power { kl_theta, .. } => {
769                assert!(
770                    kl_theta > 0.72 && kl_theta < 0.78,
771                    "θ̂ = {kl_theta} should be in (0.72, 0.78) for x⁴ (θ=3/4)"
772                );
773            }
774            other => panic!("expected Power for x⁴ descent, got {other:?}"),
775        }
776    }
777
778    /// (c) Gradient descent on x⁶ (Łojasiewicz θ = 5/6 ≈ 0.833). θ̂ ∈ (0.80,
779    /// 0.87), selected as Power.
780    #[test]
781    fn power_theta_recovered_x6() {
782        let seq = power_descent_decreases(6, 0.01, 3200);
783        let window = subsampled_window(&seq, 799, 100, 24);
784        let model = fit_rate(&window).expect("power fit x6");
785        match model {
786            RateModel::Power { kl_theta, .. } => {
787                assert!(
788                    kl_theta > 0.80 && kl_theta < 0.87,
789                    "θ̂ = {kl_theta} should be in (0.80, 0.87) for x⁶ (θ=5/6)"
790                );
791            }
792            other => panic!("expected Power for x⁶ descent, got {other:?}"),
793        }
794    }
795
796    /// (d) An oscillating sequence (an accepted-step increase) triggers the
797    /// monotonicity defect, and `assess` surfaces it as `KlInconsistent`.
798    #[test]
799    fn oscillation_triggers_monotonicity_defect() {
800        let mut window = DecreaseWindow::new();
801        window.push(1, 0.10, 0.01);
802        window.push(2, 0.05, 0.01);
803        window.push(3, -0.02, 0.01); // accepted-step INCREASE
804        window.push(4, 0.03, 0.01);
805
806        let reason = monotonicity_defect(&window, 1.0e-9).expect("defect must fire");
807        assert!(
808            reason.contains("iter 3"),
809            "defect should name the offending iter 3: {reason}"
810        );
811
812        match assess(&window, 1.0, 1.0e-3, 1.0e6) {
813            LoopVerdict::KlInconsistent { reason } => {
814                assert!(reason.contains("monotonicity defect"), "{reason}");
815            }
816            other => panic!("expected KlInconsistent from oscillation, got {other:?}"),
817        }
818
819        // A clean monotone window must NOT fire the defect.
820        let clean = geometric_window(1.0, 0.9, 10);
821        assert!(
822            monotonicity_defect(&clean, 1.0e-9).is_none(),
823            "monotone window must not report a defect"
824        );
825    }
826
827    /// (e) A total step-energy exceeding the sufficient-decrease budget
828    /// triggers the energy-budget defect; a within-budget total does not.
829    #[test]
830    fn energy_budget_violation_triggers_defect() {
831        // Budget = (V0 − V_lb)/a = (1.0 − 0.0)/1.0 = 1.0; total 10.0 > 1.0.
832        let reason = energy_budget_defect(10.0, 1.0, 0.0, 1.0).expect("defect must fire");
833        assert!(reason.contains("energy-budget defect"), "{reason}");
834
835        // Within budget: no defect.
836        assert!(
837            energy_budget_defect(0.5, 1.0, 0.0, 1.0).is_none(),
838            "within-budget energy must not report a defect"
839        );
840        // Hypotheses unmet (a ≤ 0): no defect asserted.
841        assert!(
842            energy_budget_defect(1.0e9, 1.0, 0.0, 0.0).is_none(),
843            "a ≤ 0 is outside the theorem; no defect"
844        );
845    }
846
847    /// A too-short window yields `InsufficientData`, never a spurious verdict.
848    #[test]
849    fn insufficient_data_when_window_too_short() {
850        let mut window = DecreaseWindow::new();
851        window.push(1, 0.1, 0.0);
852        window.push(2, 0.05, 0.0);
853        assert!(fit_rate(&window).is_none());
854        assert_eq!(
855            assess(&window, 1.0, 1.0e-3, 1.0e6),
856            LoopVerdict::InsufficientData
857        );
858    }
859
860    /// Lifetime Kahan accumulators track totals across ring eviction.
861    #[test]
862    fn lifetime_accumulators_survive_eviction() {
863        let mut window = DecreaseWindow::with_capacity(2);
864        window.push(1, 0.5, 4.0);
865        window.push(2, 0.25, 1.0);
866        window.push(3, 0.125, 0.25); // evicts iter 1 from the ring
867        assert_eq!(window.len(), 2);
868        assert_eq!(window.observed_count(), 3);
869        assert!((window.total_decrease() - 0.875).abs() < 1.0e-12);
870        assert!((window.total_step_norm_sq() - 5.25).abs() < 1.0e-12);
871        // Ring retains only the two most recent entries.
872        let iters: Vec<u64> = window.entries().map(|e| e.iter_index).collect();
873        assert_eq!(iters, vec![2, 3]);
874    }
875}