lyapunov_verdict tool v0.1

STEP: 1509 / 公開日: 2026-08-28 / Test: 35/35 PASS / Lean 4: 9 theorem zero sorry / Type: STEP 1497 制御理論 arc candidate #1 実装

1. 決定表

2. 使用例

import { lyapunovVerdict } from './src/mcp/lyapunov-verdict';

// A: 単調減少 → TRUE (asymptotic)
lyapunovVerdict({ series: [10, 8, 5, 3, 1] });
// { verdict: 'TRUE', reason: 'asymptotically_stable', strictDecreases: 4, ... }

// B: fixpoint 到達 → SELF
lyapunovVerdict({ series: [5, 5, 5] });
// { verdict: 'SELF', reason: 'fixpoint_reached', ... }

// C: STEP 1399 relaxation 抽象化 → TRUE (Lyapunov, plateau at end)
lyapunovVerdict({ series: [100, 80, 50, 20, 5, 1, 1, 1] });
// { verdict: 'TRUE', reason: 'lyapunov_stable', ... }

// D: 振動 → NEITHER (oscillating)
lyapunovVerdict({ series: [5, 3, 7, 4, 6] });
// { verdict: 'NEITHER', reason: 'oscillating_marginal', ... }

3. Lean 4 (9 theorem zero sorry)

lyap_both_zero_gives_zero        : (0,0) → ZERO
lyap_zero_start_diverge_false    : (0,b>0) → FALSE
lyap_fixpoint_gives_self         : (a,a) a>0 → SELF
lyap_decrease_gives_true         : ba → FALSE
all_dec_empty / all_dec_single   : 空/単一 → true
all_dec_pair / all_dec_pair_up_false : 2 要素 pair 単調性