Verified Basin
The (ω, ζ) parameter plane of the damped harmonic oscillator, coloured by whether the response stays non-negative. The horizontal white line at ζ = 1 is the theorem boundary — above it, the response is the critically-damped kernel (1 + ω·t)·exp(−ω·t) we proved sign-preserving in MachLib.Applications.SpringCriticallyDamped. Below it, the cos factor of the underdamped solution can dip the response negative — that's the framework's open territory.
click anywhere to pull the response at that (ω, ζ). Currently: underdamped (ζ < 1) · ω = 2.50 · ζ = 0.50
theorem named by the boundary
spring_critical_signpreserving (A ≥ 0, ω > 0, t ≥ 0) → result ≥ 0Lives in
foundations/MachLib/Applications/SpringCriticallyDamped.lean. Proven against MachLib's axiomatised analytic base (machlib_real_axioms, exp_pos, etc.). The ζ < 1 underdamped branch is explicitly not proven — the docstring flags it as non-claim, and the red strip on the basin shows why: the cos factor of the underdamped solution makes the response dip below zero.method
Each pixel: closed-form response with initial x(0)=1, x'(0)=0; sample at
320 points across t ∈ [0, 6]; colour by sign of min x(t). White line at ζ = 1 overlaid.Numerical, not symbolic. The basin can mis-classify points near the boundary if the response dips very shallowly between sample times — flagged only as a caveat, not a load-bearing concern. The theorem stands either way.