{"id":"palomar/PALOMAR-2026-10-11-000004","url":"https://github.com/sascha2718/lean-dual-analytic-ifs/tree/0155d92226966a90fa219bbcb9d44d2ed89d84d2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-11-000004-v2.json","repo":"https://github.com/sascha2718/lean-dual-analytic-ifs","tags":["math.DS","math.CA","math.MG","msc:28A80","msc:37C45","fractals","iterated-function-systems","dimension-theory","lean"],"score":0,"title":"Exponential separation of analytic self-conformal sets on the real line: Lean formalisation","trust":"high","domain":"math.DS","source":"palomar","authors":["Balázs Bárány","István Kolossváry","Sascha Troscheit"],"reviews":0,"subject":"math.DS","summary":"Lean 4 formalisation of exponential separation for analytic iterated function systems on the real line. Strong exponential separation holds on an open and dense subset in the C2 topology and follows from an explicit criterion involving dual projections. The development characterises conjugacy to self-similar systems and proves dimension consequences conditional on cited results of Rapaport and Bowen, including a drop in the L^q dimensions of the natural measure of a concrete three-map example.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-14","reactions":{},"formalized":true,"formalizes":[{"title":"On exponential separation of analytic self-conformal sets on the real line","identifier":"arXiv:2509.07888v3","relationship":"formalizes"}]}