{"id":"palomar/PALOMAR-2026-10-19-000011","url":"https://github.com/CoolRmal/falconer-theta-gauge/tree/98d3222b42ba5fcaeb56068cf2d542c3d4851d80","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-19-000011-v1.json","repo":"https://github.com/CoolRmal/falconer-theta-gauge","tags":["math.CA","msc:28A80","msc:42B10","harmonic-analysis","fractal-geometry","formalization"],"score":0,"title":"Falconer's distance problem for stretched logarithmic gauges","trust":"high","domain":"math.CA","source":"palomar","authors":["Yongxi Lin"],"reviews":0,"subject":"math.CA","summary":"A Lean 4 formalization of Theorem 1.1 of the supplied October 2026 manuscript: every compact subset of the Euclidean plane with positive Hausdorff measure for the gauge r exp(-(log(1/r))^theta), with 2/3 < theta < 1, has a distance set of positive Lebesgue measure. The proof constructs gauge Frostman probabilities with finite logarithmic critical and Fourier energies, obtains the required radial Orlicz densities, and decomposes the measures into finite-depth regular pieces. Measurable directional tests and smooth masks define actual filtered distance measures with summable removed mass.…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"Falconer's distance problem for the gauges r exp(-(log(1/r))^theta), theta > 2/3: a complete proof with scale-dependent parameters","identifier":"8 October 2026, Theorem 1.1, pages 2-3","relationship":"formalizes"}]}