Lyapunov certificate checking via CROWN bounds

This module provides a small certificate-checking interface for Lyapunov stability arguments.

Design:

• LyapunovCert packages bounds on a candidate Lyapunov function V and its derivative V̇ over a boxed region.
• NeuralLyapunov is an abstract interface for V and V̇ (typically defined from a network).
• The trusted boundary for this Lyapunov workflow is the oracle axiom crown_oracle, quarantined in NN.MLTheory.CROWN.Lyapunov.Oracle. Downstream theorems in this file only depend on that axiom.

The bottom portion specializes to ℝ so that strict inequalities like V_lo > 0 ⟹ V(x) > 0 can be discharged by simple order transitivity (0 < V_lo and V_lo ≤ V(x)).

theorem NN.MLTheory.CROWN.Lyapunov.v_bounded_below {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (w : CrownOracleWitness lyap cert) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.V x ≥ cert.V_lo

V is bounded below on the certified region.

theorem NN.MLTheory.CROWN.Lyapunov.v_bounded_above {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (w : CrownOracleWitness lyap cert) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.V x ≤ cert.V_hi

V is bounded above on the certified region.

theorem NN.MLTheory.CROWN.Lyapunov.vdot_bounded_below {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (w : CrownOracleWitness lyap cert) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.Vdot x ≥ cert.Vdot_lo

V̇ is bounded below on the certified region.

theorem NN.MLTheory.CROWN.Lyapunov.vdot_bounded_above {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (w : CrownOracleWitness lyap cert) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.Vdot x ≤ cert.Vdot_hi

V̇ is bounded above on the certified region.

theorem NN.MLTheory.CROWN.Lyapunov.V_bounded_below {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (w : CrownOracleWitness lyap cert) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.V x ≥ cert.V_lo

theorem NN.MLTheory.CROWN.Lyapunov.V_bounded_above {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (w : CrownOracleWitness lyap cert) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.V x ≤ cert.V_hi

theorem NN.MLTheory.CROWN.Lyapunov.Vdot_bounded_below {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (w : CrownOracleWitness lyap cert) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.Vdot x ≥ cert.Vdot_lo

theorem NN.MLTheory.CROWN.Lyapunov.Vdot_bounded_above {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (w : CrownOracleWitness lyap cert) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.Vdot x ≤ cert.Vdot_hi

theorem NN.MLTheory.CROWN.Lyapunov.quantitative_bounds {α : Type} [Context α] {n : ℕ} (lyap : NeuralLyapunov α n) (cert : LyapunovCert α n) (w : CrownOracleWitness lyap cert) : (∀ (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)), cert.region.contains x → cert.V_lo ≤ lyap.V x ∧ lyap.V x ≤ cert.V_hi) ∧ ∀ (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)), cert.region.contains x → cert.Vdot_lo ≤ lyap.Vdot x ∧ lyap.Vdot x ≤ cert.Vdot_hi

Quantitative bounds on V and Vdot over the certified region.

Specialization to ℝ

For proofs involving transitivity (V_lo > 0 implies V > 0), we specialize to ℝ which has the full Preorder/LinearOrder structure.

structure RealCert (n : ℕ) : Type

Concrete real-valued certificate format for JSON/importer-facing workflows.

• V_lo : ℝ

  Lower bound for the Lyapunov candidate V.

• V_hi : ℝ

  Upper bound for the Lyapunov candidate V.

• Vdot_lo : ℝ

  Lower bound for the orbital derivative Vdot.

• Vdot_hi : ℝ

  Upper bound for the orbital derivative Vdot.

• region_lo : Fin n → ℝ

  Lower endpoint of the certified input region, componentwise.

• region_hi : Fin n → ℝ

  Upper endpoint of the certified input region, componentwise.

noncomputable def mkCert {n : ℕ} (rc : RealCert n) : NN.MLTheory.CROWN.Lyapunov.LyapunovCert ℝ n

Convert the importer-friendly RealCert record into the canonical LyapunovCert.

theorem NN.MLTheory.CROWN.Lyapunov.Real.v_positive {n : ℕ} (lyap : NeuralLyapunov ℝ n) (cert : LyapunovCert ℝ n) (w : CrownOracleWitness lyap cert) (h_pos : cert.V_lo > 0) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.V x > 0

For ℝ: V is positive when V_lo > 0.

theorem NN.MLTheory.CROWN.Lyapunov.Real.vdot_negative {n : ℕ} (lyap : NeuralLyapunov ℝ n) (cert : LyapunovCert ℝ n) (w : CrownOracleWitness lyap cert) (h_neg : cert.Vdot_hi < 0) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.Vdot x < 0

For ℝ: V̇ is negative when Vdot_hi < 0.

theorem NN.MLTheory.CROWN.Lyapunov.Real.V_positive {n : ℕ} (lyap : NeuralLyapunov ℝ n) (cert : LyapunovCert ℝ n) (w : CrownOracleWitness lyap cert) (h_pos : cert.V_lo > 0) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.V x > 0

theorem NN.MLTheory.CROWN.Lyapunov.Real.Vdot_negative {n : ℕ} (lyap : NeuralLyapunov ℝ n) (cert : LyapunovCert ℝ n) (w : CrownOracleWitness lyap cert) (h_neg : cert.Vdot_hi < 0) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hx : cert.region.contains x) : lyap.Vdot x < 0

theorem NN.MLTheory.CROWN.Lyapunov.Real.lyapunov_conditions {n : ℕ} (lyap : NeuralLyapunov ℝ n) (cert : LyapunovCert ℝ n) (w : CrownOracleWitness lyap cert) (h_V_pos : cert.V_lo > 0) (h_Vdot_neg : cert.Vdot_hi < 0) : (∀ (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)), cert.region.contains x → lyap.V x > 0) ∧ ∀ (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)), cert.region.contains x → lyap.Vdot x < 0

For ℝ: Main Lyapunov conditions