Lyapunov oracle

We isolate the single oracle assumption used by TorchLean's Lyapunov/CROWN workflow: crown_oracle.

Everything else in the Lyapunov verification workflow should reduce to ordinary theorems that depend on this axiom, but do not introduce additional axioms.

Trust-boundary policy:

• Repo linting allowlists axiom crown_oracle only in this file.
• Downstream modules should import NN.MLTheory.CROWN.Lyapunov.Oracle (directly or via NN.MLTheory.CROWN.Lyapunov.Verification) rather than defining new trusted axioms.

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.

• V_lo : α

  Lower bound for V.

• V_hi : α

  Upper bound for V.

• Vdot_lo : α

  Lower bound for V̇.

• Vdot_hi : α

  Upper bound for V̇.

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

A neural Lyapunov function specification.

In the oracle-backed workflow, Vdot is an externally supplied decay witness; this file does not derive it from dynamics on its own.

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

  Candidate Lyapunov scalar field.

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

  Orbital derivative or decay witness associated with V.

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

Opaque witness produced by an external checker that is trusted by project policy for this workflow. It attests that the numeric bounds packaged in cert are sound for the given lyap.

This witness is intentionally not constructible inside Lean. It represents an external artifact/checker run (e.g. α/β-CROWN) that we treat as a trust boundary.

axiom NN.MLTheory.CROWN.Lyapunov.crown_oracle {α : 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

Oracle axiom: if the trusted external witness is supplied for a certificate, then the certificate bounds hold.

This is the only trusted axiom for the Lyapunov oracle approach.