{"id":"palomar/PALOMAR-2026-10-14-000010","url":"https://github.com/willmfeldman/one-phase-critical-dim/tree/d55068c8ca74db340bcb7b36c1f21a4ebf93a53c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-14-000010-v1.json","repo":"https://github.com/willmfeldman/one-phase-critical-dim","tags":["math.AP","msc:35R35","msc:49Q05","msc:35B65","free-boundary-problems","calculus-of-variations","formal-verification"],"score":0,"title":"Flatness of one-homogeneous one-phase Bernoulli minimizers in dimensions at most six","trust":"high","domain":"math.AP","source":"palomar","authors":["William M. Feldman"],"reviews":0,"subject":"math.AP","summary":"A Lean 4 formalization of the flatness half of the main theorem of the OpenAI preprint \"The critical dimension for one-phase Bernoulli minimizers\" (September 24, 2026): for 1 ≤ d ≤ 6, every nonnegative, nonzero, one-homogeneous global minimizer u of the one-phase Bernoulli energy J(v; B) = ∫_B |∇v|² + 1_{v > 0} in ℝᵈ is flat, that is, u(x) = max(⟪x, e⟫, 0) for almost every x, for some unit vector e. The minimizer class is the one of Alt and Caffarelli, written out from Mathlib definitions: on every ball B, u ∈ H¹(B) and J(u; B) ≤ J(v; B) for every v ∈ H¹(B) with v − u ∈ H¹₀(B), with weak…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-14","reactions":{},"formalized":true,"formalizes":[{"title":"The critical dimension for one-phase Bernoulli minimizers","identifier":"https://github.com/openai/math/tree/main/preprints/The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026","relationship":"formalizes"}]}