Mathlib defines cos x = (exp(ix)+exp(-ix))/2, which is not a definition via Taylor series (even though you can derive the Taylor series of cos quite easily from it). exp is defined as a Taylor series in mathlib, but it might just as easily be defined as the unique solution of a particular IVP, etc. Regardless of this, I have no idea why to you seemingly a definition via Taylor series is not a "true" definition, you could probably crack open half a dozen (rigorous) real or complex analysis texts, they're likely to define sin and cos in some such way (or, alternatively, as the single set of functions satisfying certain axioms), because defining them via geometry and making this rigorous is much harder.
I can't argue whether cos has a "geometric nature" or not, because I don't know what that means. Undoubtedly cos is useful in geometry. It is, however, used in a wide range of other domains that make absolutely no reference to geometry. mathlib's definition of cos doesn't import a single geometry definition or theorem.
Remember that the starting point of this discussion was that somebody was claiming that "pi is different in non-Euclidean geometry", which, no, even in a completely different geometry, the trigonometric functions would be useful and pi is closely related to them.
I am not understanding why you think this is at all relevant.
Its like saying a^2 + b^2 = c^2 is not geometric because it doesnt make reference to triangles. But at the end of the day, everyone understands Pythagorean theorem to be an inherently geometric equation, because geomtry is just equations and numbers.
I realize to some extent this is all subjective, but to me its insane to claim that cos is not an inherently geometric function. Agree to disagree.
You're analogy is flawed. Pythagoras' theorem is about right triangles. "a^2+b^2=c^2" isn't about triangles, it's not even a theorem, it's simply an equation (typically a diophantine one) that is satisfied by some numbers but not others. Something which typically belongs to number theory. Obviously the two things are closely related (which is the beauty of mathematics - there are a lot of connections between very different fields).
But really, I'll refer again to the part of my previous reply where I contextualise why I wrote what I wrote and how that answers the question of whether pi is somehow arbitrary due to the fact that we usually think of space as Euclidean: it's not.
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]