Is there a formalization of the link between geometry and analytical geometry? Geometry and algebra/calculus can be formalized by axioms.
Is there a global theory that combines both and establishes correspondences such as


*

*the equation of a straight line is $ax+by+c=0$,

*the length of a segment is $\sqrt{(x_b-x_a)^2+(y_b-y_a)^2}$,

*a rotation corresponds to an orthogonal transformation,

*the circumference of a unit circle is $2\pi$,
and so on. I mean not just in the numerical sense, but with an established correspondence between the equations and the geometric entities and measures as defined by Euclid.
As an application, can a geometric proof of the identity
$$\lim_{\theta\to0}\frac{\sin\theta}\theta=1$$ constitute an undisputable argument in terms of calculus ?

The "basics" are developed by Hilbert into The Foundations of Geometry (1899).
The book states the axioms for plane Euclidean geometry.
Hilbert defines the fundamental geometrical object : segment.
Indipendently, he states the laws for real numbers.
Finally, Hilbert develop an "algebra of segments", i.e defines the operations of sum and multiplication of segments, showing that they satisfy the previous laws.
With all this machinery in place :

To the system of segments already discussed, let us now add a second system. We will distinguish the segments of the new system from those of the former one by means of a special sign, and will call them “negative” segments in contradistinction to the “positive” segments already considered. If we introduce also the segment $O$, which is determined by a single point, and make other appropriate conventions, then all of the rules [previously] deduced for calculating with real numbers will hold equally well here for calculating with segments.
In a plane $\alpha$, we now take two straight lines cutting each other in $O$ at right angles as the fixed axes of rectangular co-ordinates, and lay off from $O$ upon these two straight lines the arbitrary segments $x$ and $y$. We lay off these segments upon the one side or upon the other side of $O$, according as they are positive or negative. At the extremities of $x$ and $y$, erect perpendiculars and determine the point $P$ of their intersection. The segments $x$ and $y$ are called the co-ordinates of $P$. Every point of the plane $\alpha$ is uniquely determined by its co-ordinates $x, y$, which may be positive, negative, or zero.
Let $l$ be a straight line in the plane $\alpha$, such that it shall pass through $O$ and also through a point $C$ having the co-ordinates $a, b$. If $x, y$ are the co-ordinates of any point on $l$, it follows at once from theorem 22 [ratio between corresponding sides of similar triangles] that

$a : b = x : y ,$

or

$bx − ay = 0 ,$

is the equation of the straight line $l$ .


See also : Gerard Venema, Foundations of Geometry (Pearson, 2011).
