# Failure of integer-degree harmonic dimension comparison

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

- [A counterexample to integer-degree harmonic dimension comparison](../../preprints/A-counterexample-to-integer-degree-harmonic-dimension-comparison-September-25-2026/paper.pdf)

## 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](../ComparatorChallenges/HarmonicGrowth.lean) |