Struct LyapunovCertificate 

pub struct LyapunovCertificate {
    pub initial: u64,
    pub minimum: u64,
    pub levels: u64,
    pub max_dissipation: u64,
    pub size_bound: u64,
    pub total_steps: u64,
    pub monotone: bool,
    pub strict_descent: bool,
    pub reaches_goal: bool,
}

A machine-checked certificate that a refutation’s trajectory carries a valid Lyapunov function, with the four dynamical-systems axioms verified explicitly and the resulting complexity bound.

Fields

initial: u64

V at the start of the trajectory.

minimum: u64

V at the goal (its minimum, reached at ⊥).

levels: u64

Number of distinct potential values — the length of the strict descent.

max_dissipation: u64

The most work (steps) dissipated at any single potential level.

size_bound: u64

The size bound the descent certifies: levels · max_dissipation.

total_steps: u64

The actual number of trajectory steps (≤ size_bound).

monotone: bool

Axiom 2: V never increases along the trajectory.

strict_descent: bool

Axiom 3: V strictly decreases across its level set (no level recurs — guaranteed progress).

reaches_goal: bool

Axiom 4: the trajectory reaches the goal (the refutation closes at ⊥).

Trait Implementations

impl Clone for LyapunovCertificate

fn clone(&self) -> LyapunovCertificate

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LyapunovCertificate

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for LyapunovCertificate

fn eq(&self, other: &LyapunovCertificate) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for LyapunovCertificate

impl Eq for LyapunovCertificate

impl StructuralPartialEq for LyapunovCertificate