Mathlib.Data.Real.GoldenRatio

Stream: mathlib4

[Kim Morrison]

At first I noticed that this file breaks the naming conventions, introducing gold as an abbreviation for goldenRatio in theorem names.

Then I noticed that it's unused by anything downstream

Then finally I wonder if we actually want it developed this way, with goldenRatio : ℝ.

Any thoughts?

[Violeta Hernández]

IMO contrary to popular belief, there's little special about the golden ratio. Most if not all of its properties have generalizations to other quadratic irrationals.

[Violeta Hernández]

Its relation to the Fibonacci numbers is definitely worth having, but it should be a special case of a more general result on linear recurrences.

[Violeta Hernández]

Theorems like [1; 1, 1, 1, ...] = φ or φ attaining the worst bound in Hurwitz's theorem are also worth having, but these are few and far between and don't require us to have φ as a named constant.

[Kevin Buzzard]

Violeta Hernández said:

IMO contrary to popular belief, there's little special about the golden ratio. Most if not all of its properties have generalizations to other quadratic irrationals.

It's an extremal example in the theory of rational approximation: it is basically the hardest irrational number to approximate with rationals, because of its continued fraction $[1;1,1,1,1,...]$. This is a counterexample to "all" in the sentence above.

[Violeta Hernández]

(that's the thing about Hurwitz's theorem I said, isn't it?)

[Violeta Hernández]

At least, all of the things in the current golden ratio file are either trivial or special cases of other things.

[Yury G. Kudryashov]

I think that we should have a definition for goldenRatio. Indeed, most of the theory can be generalized to a + \sqrt{b} for any a b, but goldenRatio (or goldenConj) appears in quite a few math papers on circle dynamics, because it corresponds to a fixed point of x \mapsto \{1 / x\}, which means that you can deal with renormalizations that don't change the roration number. While many (if not all) of these papers can be generalized to maps with rotation number of finite type, I don't think that we should make it even harder to formalize them.

[Yury G. Kudryashov]

BTW, I don't think that these definitions should be reducible.