# Yau’s nodal bounds: surfaces and higher dimensions

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

- [Sharp nodal length on smooth surfaces](../../preprints/Sharp-nodal-length-on-smooth-surfaces-September-23-2026/paper.pdf)
- [Smooth counterexamples to Yau's nodal upper bound in dimensions three and four](../../preprints/Smooth-counterexamples-to-Yaus-nodal-upper-bound-in-dimensions-three-and-four-September-23-2026/paper.pdf)
- [Power-law violations of Yau's nodal upper bound](../../preprints/Power-law-violations-of-Yaus-nodal-upper-bound-September-23-2026/paper.pdf)

## Scope

Yau's nodal-set conjecture predicts nodal size of order $\sqrt\lambda$ for Laplace eigenfunctions of eigenvalue $\lambda$. The formalization proves the upper bound on every fixed smooth closed connected Riemannian surface: there is a surface-dependent constant $C$ such that the one-dimensional Hausdorff measure of the zero set of every nonzero real eigenfunction with $\lambda>0$ is at most $C\sqrt\lambda$. The known lower bound is not part of this selected statement.

The formalized results contradict Yau's proposed $O(\sqrt\lambda)$ upper bound for nodal measure in dimensions three and four. On $S^3$, every prescribed smooth neighborhood of the round metric contains one fixed smooth metric with an eigenfunction sequence of unbounded nodal-measure ratio. A second fixed metric on $S^2\times T^2$ has the same property. In both cases the eigenvalues tend to infinity and the intrinsic nodal measures are finite.

Yau's nodal upper-bound conjecture predicts that the nodal measure of an eigenfunction is bounded by a constant times the square root of its eigenvalue. The formalized counterexample fixes one smooth metric on $S^4\times S^1$ and a sequence of nonzero smooth eigenfunctions whose positive eigenvalues tend to infinity, while the intrinsic four-dimensional nodal measures divided by the square roots of the eigenvalues tend to infinity. The metric is fixed throughout the sequence.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Sharp upper bound for nodal length on smooth surfaces | [NodalLength.lean](../ComparatorChallenges/NodalLength.lean) |
| Nodal counterexamples in dimensions three and four | [SmoothYau.lean](../ComparatorChallenges/SmoothYau.lean) |
| Unbounded nodal ratio on $S^4\times S^1$ | [YauCounterexample.lean](../ComparatorChallenges/YauCounterexample.lean) |