# The critical dimension for the one-phase Bernoulli problem

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The critical dimension for one-phase Bernoulli minimizers](../../preprints/The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026/The-critical-dimension-for-one-phase-Bernoulli-minimizers-September-24-2026.pdf)

## Scope

The paper identifies seven as the critical dimension for nonflat one-homogeneous global minimizers of the one-phase Bernoulli problem. The linked formalization proves the existence side: in dimension seven there is a nonzero one-homogeneous global minimizer that is not a half-space solution.

The flatness classification in dimensions at most six and the resulting regularity and singular-set bounds are outside this selected statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| A nonflat one-homogeneous Bernoulli minimizer in dimension seven | [BernoulliNonflatInSeven.lean](../ComparatorChallenges/BernoulliNonflatInSeven.lean) |