There are many equivalent definitions and many of them do not refer to geometry at all. If you don't want to go through cos you can always define pi as sqrt(6 * sum from 1 to inf 1/n^2).
You can also define it as `3.14159...` just because. Obviously, a π definition entirely divorced from geometry becomes irrelevant to it - instead, in geometry, you'd still use π = circumference/diameter, or π = whatever(cos), and those values would happen to be the same as a non-geometric π, but only if the geometric π is the one from Euclidean geometry.
There are many equivalent definitions and many of them do not refer to geometry at all. If you don't want to go through cos you can always define pi as sqrt(6 * sum from 1 to inf 1/n^2).
You can also define it as `3.14159...` just because. Obviously, a π definition entirely divorced from geometry becomes irrelevant to it - instead, in geometry, you'd still use π = circumference/diameter, or π = whatever(cos), and those values would happen to be the same as a non-geometric π, but only if the geometric π is the one from Euclidean geometry.
> You can also define it as `3.14159...` just because.
That's not a rigorous definition, though, because it doesn't tell you what those "..." expand to.
To quote myself:
> cos can be defined via its power series or via the exp function (if you use complex numbers).
Any function can be defined as a taylor series. That is not at all an argument against its geometric nature.
> Any function can be defined as a taylor series.
First of all, that's wrong. It's only true for analytic functions.
Second of all, sin and cos appear in all sorts of contexts that are not primarily geometric (such as harmonic analysis).
Lean's mathlib defines pi precisely the way I've described it - cos is defined via exp, and pi is defined as the unique zero in [0,2]
4 replies →