Function verify_lyapunov 

pub fn verify_lyapunov(
    potential: &[u64],
    reaches_goal: bool,
) -> Option<LyapunovCertificate>

Verify the four Lyapunov axioms over a potential trajectory and return the certificate, or None if any axiom fails. (1) bounded below — u64 is ≥ 0 by type; (2) monotone non-increasing; (3) strict descent across the level set; (4) reaches the minimum at the goal. A trajectory that stalls (a level recurs) or never closes is not a Lyapunov function and certifies nothing.