Lyapunov certificate semantics

This module defines the mathematical statement carried by a Lyapunov certificate. It does not turn producer-reported bounds into a theorem. A checked workflow must prove LyapunovCert.ValidFor from a verified graph evaluation or certificate checker; an external workflow must state that validity assumption at its own trust boundary.

References:

• Lyapunov stability is the classical certificate pattern: prove V > 0 and Vdot < 0 on a region.
• The numeric bound producer is CROWN-style affine/interval propagation; see Zhang et al. (CROWN, NeurIPS 2018) and Xu et al. (auto_LiRPA/α-CROWN).

structure NN.MLTheory.CROWN.Lyapunov.LyapunovCert (α : Type) [Context α] (n : ℕ) : Type

Certificate for Lyapunov verification over a boxed region.

• region : Box α (Spec.Shape.dim n Spec.Shape.scalar)

  Region on which the bounds are claimed.

• vLower : α

  Lower bound for V.

• vUpper : α

  Upper bound for V.

• derivativeLower : α

  Lower bound for V̇.

• derivativeUpper : α

  Upper bound for V̇.

structure NN.MLTheory.CROWN.Lyapunov.NeuralLyapunov (α : Type) [Context α] (n : ℕ) : Type

A neural Lyapunov function specification.

Vdot is supplied by the application; this file does not derive it from dynamics on its own.

• value : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar) → α

  Candidate Lyapunov scalar field.

• orbitalDerivative : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar) → α

  Orbital derivative or decay witness associated with V.

structure NN.MLTheory.CROWN.Lyapunov.LyapunovCert.ValidFor {α : Type} [Context α] {n : ℕ} (cert : LyapunovCert α n) (lyap : NeuralLyapunov α n) : Prop

Proof object produced by a semantic certificate checker.

Parsing a certificate or checking the signs of its endpoints cannot construct this structure. Its two fields require enclosure proofs for the actual functions named by lyap on the actual region stored in cert.

• valueBounds (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : cert.region.contains x → cert.vLower ≤ lyap.value x ∧ lyap.value x ≤ cert.vUpper

  The checked interval for the Lyapunov candidate.

• orbitalDerivativeBounds (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : cert.region.contains x → cert.derivativeLower ≤ lyap.orbitalDerivative x ∧ lyap.orbitalDerivative x ≤ cert.derivativeUpper

  The checked interval for the orbital derivative.