{"id":"palomar/PALOMAR-2026-10-27-000028","url":"https://github.com/willmfeldman/bernoulli-perron-variational/tree/2abc33271f023fcb309e6c8cd07e229a352ed911/challenges/main-results","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000028-v1.json","repo":"https://github.com/willmfeldman/bernoulli-perron-variational","tags":["math.AP","msc:35R35","msc:35D40","msc:49Q10","msc:35J25","msc:35B65"],"score":0,"title":"Perron's extremal solutions of the Bernoulli one-phase problem: viscosity, inner variational and one-sided minimizing solutions, and free boundary structure in the plane","trust":"high","domain":"math.AP","source":"palomar","authors":["William M. Feldman"],"reviews":0,"subject":"math.AP","summary":"A Lean 4 formalization of the main results of Abedin, Feldman and Stinson on Perron's extremal solutions of the one-phase Bernoulli free boundary problem Δu = 0 in {u > 0} ∩ U, |∇u| = Q on ∂{u > 0} ∩ U. Let U ⊂ ℝᵈ, d ≥ 2, be open, bounded and connected with C² boundary, and let Q be Lipschitz on the closure of U with 0 0 on ∂U is (i) a viscosity solution in U, (ii) an inner variational solution in U for some χ (the first domain variation of the Alt–Caffarelli energy ∫ |∇u|² + Q² χ vanishes), and (iii) a downward minimizer of that energy on a ball around each free boundary point; the largest…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"Variational properties of Perron's extremal solutions in the Bernoulli one-phase problem","identifier":"arXiv:2609.14981","relationship":"formalizes"}]}