NN.MLTheory.Stability.Runtime

Executable Float-specialized diagnostics for the stability specifications in NN.MLTheory.Stability.Spec.

Stability runtime utilities (Float)

This module provides executable, Float-specialized helpers for exploring stability properties of discrete-time systems (x_{t+1} = f x_t).

All routines in this file are runtime diagnostics:

• they compute concrete trajectories and check concrete inequalities, and
• they return Bool for convenience in scripts/CLIs.

They are factually correct as computations (“this inequality held on these sampled points for this many steps”), but they are not proofs of the corresponding Prop definitions in NN.MLTheory.Stability.Spec.

In other words:

• true means “passed these tests”, not “theorem proved”;
• false means “found a counterexample to the tested condition”.

def NN.MLTheory.Stability.Runtime.testLyapunovStability {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (equilibrium : Spec.Tensor Float s) (initial_points : List (Spec.Tensor Float s)) (max_iterations : ℕ) (tolerance : Float) : Bool

Empirical Lyapunov stability test:

For each initial point x₀ in initial_points, generate a length-max_iterations trajectory and check that every state stays within tolerance (in L2 distance) of equilibrium.

This is a bounded-time and finite-set check; it does not certify Lyapunov stability.

def NN.MLTheory.Stability.Runtime.testLyapunovStability.test_trajectory_bounded {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (eq x₀ : Spec.Tensor Float s) (max_iter : ℕ) (tol : Float) : Bool

def NN.MLTheory.Stability.Runtime.generateTrajectory {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (x₀ : Spec.Tensor Float s) (steps : ℕ) : List (Spec.Tensor Float s)

Generate the first steps iterates of a discrete-time system x_{t+1} = f x_t, starting at x₀.

The returned list includes the initial state x₀ as the first element (because we use scanl).

def NN.MLTheory.Stability.Runtime.testAsymptoticStability {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (equilibrium : Spec.Tensor Float s) (initial_points : List (Spec.Tensor Float s)) (max_iterations : ℕ) (convergence_threshold : Float) : Bool

Empirical asymptotic stability test (finite-horizon):

For each x₀ in initial_points, simulate max_iterations steps and check that the final state is within convergence_threshold of equilibrium (in L2 distance).

This is a very coarse check: it only inspects the last iterate and does not quantify a rate.

def NN.MLTheory.Stability.Runtime.testExponentialStability {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (equilibrium x₀ : Spec.Tensor Float s) (expected_decay_rate : Float) (max_iterations : ℕ) : Bool

Empirical exponential decay test:

We simulate a trajectory, compute distances d_t = ‖x_t - equilibrium‖₂, and check a simple inequality of the form

d_t ≤ d_0 * exp(-rate * t)

for the given expected_decay_rate.

This is a heuristic diagnostic; it is not a proof of exponential stability.

def NN.MLTheory.Stability.Runtime.testExponentialStability.test_exponential_decay (distances : List Float) (rate : Float) : Bool

def NN.MLTheory.Stability.Runtime.testContractivity {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (test_pairs : List (Spec.Tensor Float s × Spec.Tensor Float s)) (expected_contraction_factor : Float) : Bool

Empirical contractivity test on a finite list of input pairs.

Checks the inequality

‖f x - f y‖₂ / ‖x - y‖₂ ≤ expected_contraction_factor

for each pair (x,y) in test_pairs, ignoring pairs with zero input distance.

def NN.MLTheory.Stability.Runtime.testBiboStability {s₁ s₂ : Spec.Shape} (f : Spec.Tensor Float s₁ → Spec.Tensor Float s₂) (test_inputs : List (Spec.Tensor Float s₁)) (input_bound output_bound : Float) : Bool

Empirical BIBO stability test on a finite list of inputs.

For each test input x, if ‖x‖₂ ≤ input_bound then we check ‖f x‖₂ ≤ output_bound.

def NN.MLTheory.Stability.Runtime.testTrainingStability (loss_sequence : List Float) (tolerance : Float) : Bool

Empirical monotonic-loss check for a training log.

Returns true if each consecutive loss satisfies l_{t+1} ≤ l_t + tolerance.

def NN.MLTheory.Stability.Runtime.estimateStabilityMargin {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (equilibrium : Spec.Tensor Float s) (test_radii : List Float) (max_iterations : ℕ) : Float

Empirical estimate of a Lyapunov-style stability margin.

For each candidate radius r in test_radii, we generate a small finite set of points on a synthetic “sphere” of radius r around equilibrium and check a bounded-horizon Lyapunov test. The result is the maximum radius that passes these finite checks.

def NN.MLTheory.Stability.Runtime.estimateStabilityMargin.generate_points_on_sphere {s : Spec.Shape} (center : Spec.Tensor Float s) (radius : Float) (count : ℕ) : List (Spec.Tensor Float s)

def NN.MLTheory.Stability.Runtime.estimateStabilityMargin.add_spherical_perturbation {s : Spec.Shape} (center : Spec.Tensor Float s) (radius angle : Float) : Spec.Tensor Float s

structure NN.MLTheory.Stability.Runtime.StabilityAnalysisResult : Type

Results of a small battery of empirical stability diagnostics.

• isLyapunovStable : Bool

  Result of a finite-horizon Lyapunov test (test_lyapunov_stability).

• isAsymptoticallyStable : Bool

  Result of a finite-horizon asymptotic test (test_asymptotic_stability).

• isContractive : Bool

  Result of an empirical contractivity test (test_contractivity).

• isBiboStable : Bool

  Result of a BIBO check (test_bibo_stability).

• stabilityMargin : Float

  Empirical stability margin estimate (estimate_stability_margin).

• convergence_rate : Float

  Empirical convergence-rate estimate (see analyze_stability).

def NN.MLTheory.Stability.Runtime.analyzeStability {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (equilibrium : Spec.Tensor Float s) (test_points : List (Spec.Tensor Float s)) (max_iterations : ℕ) : StabilityAnalysisResult

Run a small collection of empirical stability diagnostics and summarize the results.

def NN.MLTheory.Stability.Runtime.analyzeStability.estimate_convergence_rate {s : Spec.Shape} (f : Spec.Tensor Float s → Spec.Tensor Float s) (eq x₀ : Spec.Tensor Float s) (steps : ℕ) : Float