{"id":"palomar/PALOMAR-2026-10-18-000008","url":"https://github.com/QuanyuTang/polya-szego-planar-unconditional-palomar/tree/5311f47821b5da92e81e75b7da5091d176c8deb9","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000008-v1.json","repo":"https://github.com/QuanyuTang/polya-szego-planar-unconditional-palomar","tags":["math.AP","spectral-theory","buckling-eigenvalue","lean","pdes"],"score":0,"title":"Planar Pólya–Szegő Buckling Inequality","trust":"high","domain":"math.AP","source":"palomar","authors":["Quanyu Tang","Haiqi Zhang"],"reviews":0,"subject":"math.AP","summary":"Lean formalization proving the planar Polya-Szego conjecture for the first buckling eigenvalue. For open planar sets of positive finite area, it proves the sharp area inequality and characterizes equality by exact equality with an open disk. It retains the original Sobolev-space, variational eigenvalue and Bessel definitions, and includes the disk eigenvalue and buckling–Dirichlet comparison.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"A sharp comparison between planar buckling and Dirichlet eigenvalues","identifier":"","relationship":"formalizes"}]}