Failure of integer-degree harmonic dimension comparison

2 papersLean

Disproves Yau's proposed Euclidean dimension bound for harmonic functions of integer growth on manifolds with nonnegative Ricci curvature. For every sufficiently large integer k, a complete smooth metric on ℝ³ has at least \((k+2)^2\) independent harmonic functions of growth at most k, exceeding the Euclidean count \((k+1)^2\). The metric may depend on k.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

A counterexample to integer-degree harmonic dimension comparison

OpenAI · September 25, 2026

For some even n ≥ 8 and integer k ≥ 2, we construct a complete smooth metric on ℝⁿ with nonnegative Ricci curvature whose space of real harmonic functions of pointwise polynomial growth at most k has dimension larger than the Euclidean harmonic-polynomial dimension. The metric is Euclidean near the origin, has asymptotic volume ratio strictly between zero and one, and has nonunique tangent cones at infinity. This answers the integer-degree form of Yau's dimension comparison question in the negative.

Read PDF Download Source

Cite

@misc{OAI:A-counterexample-to-integer-degree-harmonic-dimension-comparison-September-25-2026,
  author = {{OpenAI}},
  title = {{A counterexample to integer-degree harmonic dimension comparison}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-counterexample-to-integer-degree-harmonic-dimension-comparison-September-25-2026/paper.pdf}{OAI:A-counterexample-to-integer-degree-harmonic-dimension-comparison-September-25-2026}},
  year = {2026}
}

A Three-Dimensional Counterexample to Integer-Degree Harmonic Dimension Comparison

OpenAI · September 26, 2026

For every \(4/9\lt v\lt 1\) and \(1\lt c\lt 9v/4\), all sufficiently large integers k admit a complete smooth metric on ℝ³ with nonnegative Ricci curvature, asymptotic volume ratio v, and at least \(c(k+1)^2\) linearly independent real harmonic functions of pointwise growth at most k. This answers Yau's integer-degree dimension comparison question negatively in dimension three, with a fixed-factor excess over the Euclidean count. For each \(1\lt c\lt 9/4\), these metrics can be chosen arbitrarily close to the Euclidean metric in global bi-Lipschitz distance. The metric may depend on k.

Read PDF Download Source

Cite

@misc{OAI:A-Three-Dimensional-Counterexample-to-Integer-Degree-Harmonic-Dimension-Comparison-September-26-2026,
  author = {{OpenAI}},
  title = {{A Three-Dimensional Counterexample to Integer-Degree Harmonic Dimension Comparison}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Three-Dimensional-Counterexample-to-Integer-Degree-Harmonic-Dimension-Comparison-September-26-2026/paper.pdf}{OAI:A-Three-Dimensional-Counterexample-to-Integer-Degree-Harmonic-Dimension-Comparison-September-26-2026}},
  year = {2026}
}

What was formalized in Lean

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

A counterexample to integer-degree harmonic dimension comparison

Scope

The formalized result disproves the proposed Euclidean upper comparison for dimensions of harmonic functions with integer polynomial growth. It constructs one complete smooth metric with nonnegative Ricci curvature on an even-dimensional Euclidean space, Euclidean near the origin and with asymptotic volume ratio strictly between zero and one, admitting more independent harmonic functions of the prescribed growth degree than the Euclidean count. The construction uses dimension \(16\) and degree \(50000\). Separate tangent-cone and cone-spectrum conclusions are not included.

Comparator links

Result	Comparator statement
Counterexample to harmonic dimension comparison	HarmonicGrowth.lean

Scope note on GitHub →