{"id":"palomar/PALOMAR-2026-10-19-000002","url":"https://github.com/MrGodfrey/LeanForCriteriaForLinearStochastic/tree/c088eb9943197e88c4b046223239d4c4f0180513/formalization","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-19-000002-v1.json","repo":"https://github.com/MrGodfrey/LeanForCriteriaForLinearStochastic","tags":["math.OC","math.PR","msc:93B05","msc:93E03","msc:60H10","msc:68V20","controllability","stochastic-systems","lean"],"score":0,"title":"A Unified Kalman-Type Classification of Controllability for Linear Stochastic Systems","trust":"high","domain":"math.OC","source":"palomar","authors":["Yu Wang"],"reviews":0,"subject":"math.OC","summary":"Formalization of a finite algebraic classification of approximate, approximate null, exact null, and exact controllability for finite-dimensional linear stochastic systems with constant coefficients and independent Brownian drivers. A decreasing subspace sequence gives a common obstruction for the first three properties; exact controllability additionally requires full row rank of the stacked diffusion-control matrix. The development also covers stochastic integration, forward and backward equations, duality, finite rank tests, null feedback, and polynomial small-time energy bounds. The…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"A Unified Kalman-Type Classification of Controllability for Linear Stochastic Systems","identifier":"","relationship":"formalizes"}]}