pid_tuning_verdict tool v0.1

STEP: 1531 / Test: 30/30 PASS / Lean 4: 3 theorem zero sorry / Type: STEP 1497 制御 2nd tool (47 defer 18 番目、姉妹 tool 21)

❶ PID gain (Kp, Ki, Kd) → damping ratio ζ = Kd / (2·√Kp) → verdict。単純 2 次系の damping analysis。

❂ 6 case 決定表 (7 verdict 使用): Kp=0 → ZERO / ζ≥1 → TRUE (over/critical) / 0<ζ<1 → BOTH (under-damped) / ζ=0+Ki>0 → INFINITY (windup) / ζ=0 → SELF (pure oscillation)。

決定表

Condition	Verdict	Reason
invalid gains (negative)	NEITHER	invalid_input
Kp = 0	ZERO	no_proportional_control
ζ ≥ 1 (over/critical)	TRUE	over_or_critically_damped
0 < ζ < 1	BOTH	under_damped_oscillation
ζ = 0 + Ki > 0	INFINITY	integrator_windup_risk
ζ = 0 + Ki = 0	SELF ★	sustained_oscillation

使用例

// Critical damping: Kp=1, Kd=2 → ζ = 1
pidTuningVerdict({ Kp: 1, Kd: 2 });
// { verdict: 'TRUE', reason: 'over_or_critically_damped', dampingRatio: 1 }

// Under-damped: Kp=4, Kd=1 → ζ = 0.25
pidTuningVerdict({ Kp: 4, Kd: 1 });
// { verdict: 'BOTH', reason: 'under_damped_oscillation' }

// Pure oscillation: Kp=1 only → ζ = 0
pidTuningVerdict({ Kp: 1 });
// { verdict: 'SELF', reason: 'sustained_oscillation' } ★

// Integrator windup risk
pidTuningVerdict({ Kp: 1, Ki: 1 });
// { verdict: 'INFINITY', reason: 'integrator_windup_risk' }

Lean 4 (3 theorem zero sorry)

pid_no_kp_gives_zero               : Kp=0 → ZERO
pid_integrator_windup_gives_infinity : Kd=0 + Ki>0 → INFINITY
pid_pure_oscillation_gives_self    : Kd=0 + Ki=0 → SELF ★

Honest scope

❶ 単純 2 次系 approximation のみ、 real transfer function analysis 未 embed。

❂ Ziegler-Nichols tuning / IMC / lambda tuning 未 embed、 damping ratio 基準のみ。

❸ 累計 defer 31 → 30。