{"id":"palomar/PALOMAR-2026-09-15-000007","url":"https://github.com/scottnarmstrong/MarkovProcess/tree/dbade0d12c4f84179441a9df7d7147df7a8bcaa0","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-15-000007-v1.json","repo":"https://github.com/scottnarmstrong/MarkovProcess","tags":["math.PR","msc:60J25","msc:60J35","msc:60G17","markov-processes","stochastic-analysis","lean-formalization"],"score":0,"title":"MarkovProcess","trust":"high","domain":"math.PR","source":"palomar","authors":["Scott Armstrong"],"reviews":0,"subject":"math.PR","summary":"A Lean formalization of continuous-path Markov processes associated with conservative Feller transition semigroups on nonempty locally compact Polish spaces. A uniform Kolmogorov displacement-moment bound yields a unique measurable kernel from each starting point to continuous-path space, with the prescribed finite-dimensional distributions. The library also develops strong Markov properties, generators and resolvents, stopping and killing, and Brownian motion as an example. The existence and uniqueness theorem is independently checked using Audit/ContinuousMarkovProcess/comparator.json.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-15","reactions":{},"formalized":true,"formalizes":[{"title":"Markov Processes: Characterization and Convergence","identifier":"doi:10.1002/9780470316658","relationship":"adapts"},{"title":"Continuous Martingales and Brownian Motion","identifier":"doi:10.1007/978-3-662-06400-9","relationship":"adapts"}]}