Flatness of one-homogeneous one-phase Bernoulli minimizers in dimensions at most six
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-14-000010
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-14-000010/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-14-000010/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'