avewright/proofwiki-math huggingface dataset:
Theorem: Equation of Deltoid

The point $P = \tuple {x, y}$ is described by the parametric equation:
:$\begin{cases}
x & = 2 b \cos \theta + b \cos 2 \theta \\
y & = 2 b \sin \theta - b \sin 2 \theta
\end{cases}$
where $\theta$ is the angle between the $x$-axis and the line joining the origin to the center of $C_1$.

Proof:
By definition, a deltoid is a hypocycloid with $3$ cusps.
:400px
By Equation of Hypocycloid, the equation of $H$ is given by:
:$\begin{cases}
x & = \paren {a - b} \cos \theta + b \map \cos {\paren {\dfrac {a - b} b} \theta} \\
y & = \paren {a - b} \sin \theta - b \map \sin {\paren {\dfrac {a - b} b} \theta}
\end{cases}$
From Number of Cusps of Hypocycloid from Integral Ratio of Circle Radii, this can be generated by a epicycle $C_1$ of radius $\dfrac 1 3$ the radius of the deferent.
Thus $a = 3 b$ and the equation of $H$ is now given by:
:$\begin{cases}
x & = 2 b \cos \theta + b \cos 2 \theta \\
y & = 2 b \sin \theta - b \sin 2 \theta
\end{cases}$
{{qed}}
Theorem: Equation of Epicycloid

Let a circle $C_1$ of radius $b$ roll without slipping around the outside of a circle $C_2$ of radius $a$.
Let $C_2$ be embedded in a cartesian plane with its center $O$ located at the origin.
Let $P$ be a point on the circumference of $C_1$.
Let $C_1$ be initially positioned so that $P$ is its point of tangency to $C_2$, located at point $A = \tuple {a, 0}$ on the $x$-axis.
Let $H$ be the epicycloid traced out by the point $P$.
Let $\tuple {x, y}$ be the coordinates of $P$ as it travels over the plane.
The point $P = \tuple {x, y}$ is described by the equations:
{{begin-eqn}}
{{eqn | l = x
      | r = \paren {a + b} \cos \theta - b \map \cos {\paren {\dfrac {a + b} b} \theta}
}}
{{eqn | l = y
      | r = \paren {a + b} \sin \theta - b \map \sin {\paren {\dfrac {a + b} b} \theta}
}}
{{end-eqn}}

Proof:
:600px
Let $C_1$ have rolled so that the line $OC$ through the radii of $C_1$ and $C_2$ is at angle $\theta$ to the $x$-axis.
Let $C_1$ have turned through an angle $\phi$ to reach that point.
By definition of sine and cosine, $P = \tuple {x, y}$ is defined by:
{{begin-eqn}}
{{eqn | l = x
      | r = \paren {a + b} \cos \theta - b \map \cos {\phi + \theta}
}}
{{eqn | l = y
      | r = \paren {a + b} \sin \theta - b \map \sin {\phi + \theta}
}}
{{end-eqn}}
The arc of $C_1$ between $P$ and $B$ is the same as the arc of $C_2$ between $A$ and $B$.
Thus by Arc Length of Sector:
:$a \theta = b \phi$
Thus:
:$\phi + \theta = \paren {\dfrac {a + b} b} \theta$
whence the result.
{{qed}}
Theorem: Relation between Equations for Hypocycloid and Epicycloid

Consider the hypocycloid defined by the equations:
:$x = \paren {a - b} \cos \theta + b \map \cos {\paren {\dfrac {a - b} b} \theta}$
:$y = \paren {a - b} \sin \theta - b \map \sin {\paren {\dfrac {a - b} b} \theta}$
By replacing $b$ with $-b$, this converts to the equations which define an epicycloid:
:$x = \paren {a + b} \cos \theta - b \map \cos {\paren {\dfrac {a + b} b} \theta}$
:$y = \paren {a + b} \sin \theta - b \map \sin {\paren {\dfrac {a + b} b} \theta}$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | r = \paren {a - \paren {-b} } \cos \theta + \paren {-b} \map \cos {\paren {\dfrac {a - \paren {-b} } {\paren {-b} } } \theta}
      | c = putting $-b$ for $b$
}}
{{eqn | r = \paren {a + b} \cos \theta - b \map \cos {-\paren {\dfrac {a + b} b} \theta}
      | c = 
}}
{{eqn | r = \paren {a + b} \cos \theta - b \map \cos {\paren {\dfrac {a + b} b} \theta}
      | c = Cosine Function is Even
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = y
      | r = \paren {a - \paren {-b} } \sin \theta - \paren {-b} \map \sin {\paren {\dfrac {a - \paren {-b} } {\paren {-b} } } \theta}
      | c = putting $-b$ for $b$
}}
{{eqn | r = \paren {a + b} \sin \theta + b \map \sin {-\paren {\dfrac {a + b} b} \theta}
      | c = 
}}
{{eqn | r = \paren {a + b} \sin \theta - b \map \sin {\paren {\dfrac {a + b} b} \theta}
      | c = Sine Function is Odd
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Nephroid

The point $P = \tuple {x, y}$ is described by the parametric equation:
:$\begin{cases} x & = 3 b \cos \theta - b \cos 3 \theta \\ y & = 3 b \sin \theta - b \sin 3 \theta \end{cases}$
where $\theta$ is the angle between the $x$-axis and the line joining the origin to the center of $C_1$.

Proof:
By definition, a nephroid is an epicycloid with $2$ cusps.
:600px
By Equation of Epicycloid, the equation of $H$ is given by:
:$\begin{cases} x & = \paren {a + b} \cos \theta - b \map \cos {\paren {\dfrac {a + b} b} \theta} \\ y & = \paren {a + b} \sin \theta - b \map \sin {\paren {\dfrac {a + b} b} \theta} \end{cases}$
When $a = 2 b$ the equation of $H$ is now given by:
:$\begin{cases} x & = 3 b \cos \theta - b \cos 3 \theta \\ y & = 3 b \sin \theta - b \sin 3 \theta \end{cases}$
{{qed}}
Theorem: Length of Arc of Nephroid

The total length of the arcs of a nephroid constructed around a deferent of radius $a$ is given by:
:$\LL = 12 a$

Proof:
Let a nephroid $H$ be embedded in a cartesian plane with its center at the origin and its cusps positioned at $\tuple {\pm a, 0}$.
:600px
We have that $\LL$ is $2$ times the length of one arc of the nephroid.
From Arc Length for Parametric Equations:
:$\ds \LL = 2 \int_{\theta \mathop = 0}^{\theta \mathop = \pi} \sqrt {\paren {\frac {\d x} {\d \theta} }^2 + \paren {\frac {\d y} {\d \theta} }^2} \rd \theta$
where, from Equation of Nephroid:
:<nowiki>$\begin{cases}
x & = 3 b \cos \theta - b \cos 3 \theta \\
y & = 3 b \sin \theta - b \sin 3 \theta
\end{cases}$</nowiki>
We have:
{{begin-eqn}}
{{eqn | l = \frac {\d x} {\d \theta}
      | r = -3 b \sin \theta + 3 b \sin 3 \theta
      | c = 
}}
{{eqn | l = \frac {\d y} {\d \theta}
      | r = 3 b \cos \theta - 3 b \cos 3 \theta
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {\frac {\d x} {\d \theta} }^2 + \paren {\frac {\d y} {\d \theta} }^2
      | c = 
}}
{{eqn | r = \paren {-3 b \sin \theta + 3 b \sin 3 \theta}^2 + \paren {3 b \cos \theta - 3 b \cos 3 \theta}^2
      | c = 
}}
{{eqn | r = 9 b^2 \paren {\paren {-\sin \theta + \sin 3 \theta}^2 + \paren {\cos \theta - \cos 3 \theta}^2}
      | c = 
}}
{{eqn | r = 9 b^2 \paren {\sin^2 \theta - 2 \sin \theta \sin 3 \theta + \sin^2 3 \theta + \cos^2 \theta - 2 \cos \theta \cos 3 \theta + \cos^2 3 \theta}
      | c = Square of Difference
}}
{{eqn | r = 9 b^2 \paren {2 - 2 \sin \theta \sin 3 \theta - 2 \cos \theta \cos 3 \theta}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = 18 b^2 \paren {1 - \paren {\sin \theta \sin 3 \theta + \cos \theta \cos 3 \theta} }
      | c = 
}}
{{eqn | r = 18 b^2 \paren {1 - \cos 2 \theta}
      | c = Cosine of Difference
}}
{{eqn | r = 18 b^2 \paren {2 \sin^2 \theta}
      | c = Square of Sine
}}
{{eqn | r = 36 b^2 \sin^2 \theta
      | c = simplifying
}}
{{end-eqn}}
Thus:
:$\sqrt {\paren {\dfrac {\d x} {\d \theta} }^2 + \paren {\dfrac {\d y} {\d \theta} }^2} = 6 b \sin \theta$
So:
{{begin-eqn}}
{{eqn | l = \LL
      | r = 2 \int_0^\pi 6 b \sin \theta \rd \theta
      | c = 
}}
{{eqn | r = 12 b \int_0^\pi \sin \theta \rd \theta
      | c = 
}}
{{eqn | r = 12 b \bigintlimits {-\cos \theta} 0 \pi
      | c = 
}}
{{eqn | r = 12 b \paren {-\cos \pi - \paren {-\cos 0} }
      | c = 
}}
{{eqn | r = 12 b \paren {-\paren {-1} - \paren {-1} }
      | c = 
}}
{{eqn | r = 24 b
      | c = 
}}
{{eqn | r = 12 a
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Supremum of Meet Image of Directed Set

Let $\struct {S, \preceq}$ be an up-complete meet semilattice.
Let $f: S \times S \to S$ be a mapping such that:
:$\forall \tuple {x, y} \in S \times S: \map f {x, y} = x \wedge y$
Let $D$ be directed subset of $S \times S$ in the simple order product $\struct {S \times S, \precsim}$ of $\struct {S, \preceq}$ and $\struct {S, \preceq}$.
Then:
:$\map \sup {\map {f^\to} D} = \sup \set {x \wedge y: x \in \map {\pr_1^\to} D, y \in \map {\pr_2^\to} D}$
where
:$\pr_1$ denotes the first projection on $S \times S$
:$\pr_2$ denotes the second projection on $S \times S$
:$\map {\pr_1^\to} D$ denotes the image of $D$ under $\pr_1$.

Proof:
By definition of image of set:
:$\map {f^\to} D = \set {x \wedge y: \tuple {x, y} \in D}$
By definition of subset:
:$\map {f^\to} D \subseteq \set {x \wedge y: x \in \map {\pr_1^\to} D, y \in \map {\pr_2^\to} D}$
By Up-Complete Product/Lemma 2:
:$D_1 := \map {\pr_1^\to} D$ is directed
and
:$D_2 := \map {\pr_2^\to} D$ is directed.
By Meet of Directed Subsets is Directed:
:$\set {x \wedge y: x \in D_1, y \in D_2}$ is directed.
By definition of up-complete:
:$\set {x \wedge y: x \in D_1, y \in D_2}$ admits a supremum.
By Meet is Increasing:
:$f$ is increasing mapping.
By Image of Directed Subset under Increasing Mapping is Directed:
:$\map {f^\to} D$ is directed.
By definition of up-complete:
:$\map {f^\to} D$ admits a supremum.
By Supremum of Subset:
:$\map \sup {\map {f^\to} D} \preceq \sup \set {x \wedge y: x \in D_1, y \in D_2}$
We will prove that
:$\set {x \wedge y: x \in D_1, y \in D_2} \subseteq \paren {\map {f^\to} D}^\preceq$
where
:$\paren {\map {f^\to} D}^\preceq$ denotes the lower closure of $\map {f^\to} D$.
Let $z \in \set {x \wedge y: x \in D_1, y \in D_2}$.
Then
:$\exists x \in D_1, y \in D_2: z = x \wedge y$
By definition of image of set:
:$\exists \tuple {a, b} \in D: \map {\pr_1} {a, b} = x$
and
:$\exists \tuple {c, d} \in D: \map {\pr_2} {c, d} = y$:
By definition of first projection and second projection:
:$a = x$ and $d = y$
By definition of directed subset:
:$\exists \tuple {g, h} \in D: \tuple {x, b} \precsim \tuple {g, h} \land \tuple {c, y} \precsim \tuple {g, h}$
By definition of simple order product:
:$x \preceq g$ and $y \preceq h$
By Meet Semilattice is Ordered Structure:
:$x \wedge y \preceq g \wedge h \in \set {x \wedge y: \tuple {x, y} \in D}$
Thus by definition of lower closure:
:$z \in \paren {\map {f^\to} D}^\preceq$
{{qed|lemma}}
By Supremum of Lower Closure of Set:
:$\paren {\map {f^\to} D}^\preceq$ admits a supremum
and
:$\map \sup {\map {f^\to} D}^\preceq = \map \sup {\map {f^\to} D}$
By Supremum of Subset:
:$\sup \set {x \wedge y: x \in D_1, y \in D_2} \preceq \map \sup {\map {f^\to} D}$
Thus by definition of antisymmetry:
:$\map \sup {\map {f^\to} D} = \sup \set {x \wedge y: x \in D_1, y \in D_2}$
{{qed}}
Theorem: Meet is Increasing

Let $\struct {S, \preceq}$ be a meet semilattice.
Let $f: S \times S \to S$ be a mapping such that:
:$\forall s, t \in S: \map f {s, t} = s \wedge t$
Then:
:$f$ is increasing as a mapping from the simple order product $\struct {S \times S, \precsim}$ of $\struct {S, \preceq}$ and $\struct {S, \preceq}$ into $\struct {S, \preceq}$.

Proof:
Let $\tuple {x, y}, \tuple {z, t} \in S \times S$ such that:
:$\tuple {x, y} \precsim \tuple {z, t}$
By definition of simple order product:
:$x \preceq z$ and $y \preceq t$
By Meet Semilattice is Ordered Structure:
:$x \wedge y \preceq z \wedge t$
By definition of $f$:
:$\map f {x, y} \preceq \map f {z, t}$
Thus by definition:
:$f$ is increasing mapping.
{{qed}}
Theorem: Meet Preserves Directed Suprema/Lemma 2

Let $x$ be an element of $S$, $D$ be a directed subset of $S$.
Then:
:$\paren {\sup D} \wedge x = \sup \set {d \wedge x: d \in D}$

Proof:
By Meet Precedes Operands:
:$\paren {\sup D} \wedge x \preceq \sup D$
By assumption:
:$\paren {\sup D} \wedge x \preceq \sup \set {\paren {\sup D} \wedge x \wedge d: d \in D}$
By definition of supremum:
:$\forall d \in D: d \preceq \sup D$
By Preceding iff Meet equals Less Operand:
:$\forall d \in D: d \wedge \sup D = d$
By Meet is Associative and Meet is Commutative:
:$\paren {\sup D} \wedge x \preceq \sup \set {d \wedge x: d \in D}$
By Meet Semilattice is Ordered Structure:
:$\forall d \in D: d \wedge x \preceq \paren {\sup D} \wedge x$
By definition:
:$\paren {\sup D} \wedge x$ is upper bound for $\set {d \wedge x: d \in D}$
By definition of supremum:
:$\sup \set {d \wedge x: d \in D} \preceq \paren {\sup D} \wedge x$
if $\set {d \wedge x: d \in D}$ admits a supremum
We will prove that:
:$\set {d \wedge x: d \in D}$ is directed
Let $y, z \in \set {d \wedge x: d \in D}$.
Then
:$\exists d_1 \in D: y = d_1 \wedge x$
and
:$\exists d_2 \in D: z = d_2 \wedge x$
By definition of directed subset:
:$\exists d \in D: d_1 \preceq d \land d_2 \preceq d$
By Meet Semilattice is Ordered Structure:
:$y \preceq d \wedge x$ and $z \preceq d \wedge x$
Thus
:$d \wedge x \in \set {d \wedge x: d \in D}$
Hence by definition:
:$\set {d \wedge x: d \in D}$ is directed.
{{qed|lemma}}
By definition of up-complete:
:$\set {d \wedge x: d \in D}$ admits a supremum
Thus by definition of antisymmetry:
:$\paren {\sup D} \wedge x = \sup \set {d \wedge x: d \in D}$
{{qed}}
Theorem: Supremum by Suprema of Directed Set in Simple Order Product

Let $\struct {S, \preceq}$ be an up-complete meet semilattice.
Let $\struct {S \times S, \precsim}$ be the simple order product of $\struct {S, \preceq}$ and $\struct {S, \preceq}$.
Let $D$ be a directed subset of $S \times S$.
Then:
:$\sup D = \tuple {\map \sup {\map {\pr_1^\to} D}, \map \sup {\map {\pr_2^\to} D} }$

Proof:
By Up-Complete Product:
:$\struct {S \times S, \precsim}$ is up-complete.
By definition of up-complete:
:$D$ admits a supremum.
By definition of Cartesian product:
:$\exists d_1, d_2 \in S: \sup D = \tuple {d_1, d_2}$
By Up-Complete Product/Lemma 2:
:$D_1 := \map {\pr_1^\to} D$ is directed
and
:$D_2 := \map {\pr_2^\to} D$ is directed.
By definition of up-complete:
:$D_1$ admits a supremum
and
:$D_2$ admits a supremum
We will prove that
:$d_2$ is upper bound for $D_2$
Let $x \in D_2$.
By definition of image of set:
:$\exists \tuple {a, b} \in D: \map {\pr_2} {a, b} = x$
By definition of second projection:
$b = x$
By definition of supremum:
:$\tuple {d_1, d_2}$ is upper bound for $D$.
By definition of upper bound:
:$\tuple {a, x} \precsim \tuple {d_1, d_2}$
Thus by definition of simple order product:
:$x \preceq d_2$
{{qed|lemma}}
Analogically we have that
:$d_1$ is upper bound for $D_1$
By definition of supremum:
:$\sup D_1 \preceq d_1$ and $\sup D_2 \preceq d_2$
By definition of simple order product:
:$\tuple {\sup D_1, \sup D_2} \precsim \sup D$
By Up-Complete Product/Lemma 1:
:$D_1 \times D_2$ is directed.
By definition of up-complete:
:$D_1 \times D_2$ admits a supremum.
By definition of subset:
:$D \subseteq D_1 \times D_2$
By Supremum of Subset:
:$\sup D \precsim \map \sup {D_1 \times D_2}$
By Supremum of Simple Order Product:
:$\sup D \precsim \tuple {\sup D_1, \sup D_2}$
Thus by definition of antisymmetry:
:$\sup D = \tuple {\sup D_1, \sup D_2}$
{{qed}}
Theorem: Evolute of Circle is its Center

The evolute of a circle is a single point: its center.

Proof:
By definition, the evolute of $C$ is the locus of the centers of curvature of each point on $C$
{{WLOG}}, take the circle $C$ of radius $a$ whose center is positioned at the origin of a cartesian plane.
From Equation of Circle, $C$ has the equation:
:$x^2 + y^2 = a^2$
From the definition of curvature in cartesian form:
:$k = \dfrac {y' '} {\paren {1 + y'^2}^{3/2} }$
Here we have:
{{begin-eqn}}
{{eqn | l = 2 x + 2 y \frac {\d y} {\d x}
      | r = 0
      | c = differentiating {{WRT|Differentiation}} $x$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = -\frac x y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d^2 y} {\d x^2}
      | r = \frac {x \frac {\d y} {\d x} - y} {y^2}
      | c = Quotient Rule for Derivatives
}}
{{eqn | r = \frac {y - x \paren {-\frac x y} } {y^2}
      | c = substituting for $\dfrac {\d y} {\d x}$
}}
{{eqn | r = \frac {y^2 + x^2} {y^3}
      | c = simplifying
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = k
      | r = \dfrac {\frac {y^2 + x^2} {y^3} } {\paren {1 + \paren {-\frac x y}^2}^{3/2} }
      | c = 
}}
{{eqn | r = \dfrac {y^2 + x^2} {y^3 \paren {1 + \frac {x^2} {y^2} }^{3/2} }
      | c = 
}}
{{eqn | r = \dfrac {y^2 + x^2} {y^3 \paren {\frac {y^2 + x^2} {y^2} }^{3/2} }
      | c = 
}}
{{eqn | r = \dfrac {y^2 + x^2} {\paren {y^2 + x^2}^{3/2} }
      | c = 
}}
{{eqn | r = \dfrac 1 {\paren {y^2 + x^2}^{1/2} }
      | c = 
}}
{{eqn | r = \dfrac 1 a
      | c = as $x^2 + y^2 = a^2$
}}
{{end-eqn}}
Thus the curvature of $C$ is constant.
The radius of curvature of $C$ is likewise constant:
:$\rho = a$
From Radius at Right Angle to Tangent, the normal to $C$ at all points on $C$ passes through the center of $C$.
We have that $a$ is the distance from $C$ to the center of $C$.
Thus it follows that the center of curvature of $C$ is the center of $C$ at all points.
Hence the result by definition of evolute.
{{qed}}
Theorem: Radius of Curvature in Cartesian Form

Let $C$ be a curve defined by a real function which is twice differentiable.
Let $C$ be embedded in a cartesian plane.
The '''radius of curvature''' $\rho$ of $C$ at a point $P = \tuple {x, y}$ is given by:
:$\rho = \dfrac {\paren {1 + y'^2}^{3/2} } {\size {y' '} }$
where:
:$y' = \dfrac {\d y} {\d x}$ is the derivative of $y$ {{WRT|Differentiation}} $x$ at $P$
:$y' ' = \dfrac {\d^2 y} {\d x^2}$ is the second derivative of $y$ {{WRT|Differentiation}} $x$ at $P$.

Proof:
By definition, the radius of curvature $\rho$ is given by:
:$\rho = \dfrac 1 {\size \kappa}$
where $\kappa$ is the curvature, given in Cartesian form as:
:$\kappa = \dfrac {y' '} {\paren {1 + y'^2}^{3/2} }$
As $\paren {1 + y'^2}^{3/2}$ is positive, it follows that:
:$\size {\dfrac {y' '} {\paren {1 + y'^2}^{3/2} } } = \dfrac {\size {y' '} } {\paren {1 + y'^2}^{3/2} }$
Hence the result.
{{qed}}
Theorem: Parametric Equations for Evolute/Formulation 1

Let $C$ be a curve expressed as the locus of an equation $\map f {x, y} = 0$.
The parametric equations for the evolute of $C$ can be expressed as:
:<nowiki>$\begin{cases}
X = x - \dfrac {y' \paren {1 + y'^2} } {y' '} \\
Y = y + \dfrac {1 + y'^2} {y''}
\end{cases}$</nowiki>
where:
:$\tuple {x, y}$ denotes the Cartesian coordinates of a general point on $C$
:$\tuple {X, Y}$ denotes the Cartesian coordinates of a general point on the evolute of $C$
:$y'$ and $y' '$ denote the derivative and second derivative respectively of $y$ {{WRT|Differentiation}} $x$.

Proof:
:400px
Let $P = \tuple {x, y}$ be a general point on $C$.
Let $Q = \tuple {X, Y}$ be the center of curvature of $C$ at $P$.
From the above diagram:
:$x - X = \pm \rho \sin \psi$
:$Y - y = \pm \rho \cos \psi$
where:
:$\rho$ is the radius of curvature of $C$ at $P$
:$\psi$ is the angle between the tangent to $C$ at $P$ and the $x$-axis.
Whether the sign is plus or minus depends on whether the curve is convex or concave.
By definition of radius of curvature:
:$(1): \quad \begin {cases} x - X = \dfrac 1 k \sin \psi \\ Y - y = \dfrac 1 k \cos \psi \end {cases}$
where $k$ is the curvature of $C$ at $P$, given by:
:$k = \dfrac {y' '} {\paren {1 + y'^2}^{3/2} }$
We have that:
:$\sin \psi = \dfrac {\d y} {\d s} = \dfrac {y'} {\sqrt {1 + y'^2} }$
:$\cos \psi = \dfrac {\d x} {\d s} = \dfrac 1 {\sqrt {1 + y'^2} }$
Substituting for $k$ and $\psi$ in $(1)$ gives:
{{begin-eqn}}
{{eqn | l = x - X
      | r = \dfrac {\paren {1 + y'^2}^{3/2} } {y' '} \dfrac {y'} {\sqrt {1 + y'^2} }
      | c = 
}}
{{eqn | r = \dfrac {y' \paren {1 + y'^2} } {y' '}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = X
      | r = x - \dfrac {y' \paren {1 + y'^2} } {y' '}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = Y - y
      | r = \dfrac {\paren {1 + y'^2}^{3/2} } {y' '} \dfrac 1 {\sqrt {1 + y'^2} }
      | c = 
}}
{{eqn | r = \dfrac {1 + y'^2} {y' '}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = Y
      | r = y + \dfrac {1 + y'^2} {y' '}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Parametric Equations for Evolute/Formulation 2

Let $C$ be a curve expressed as the locus of an equation $\map f {x, y} = 0$.
The parametric equations for the evolute of $C$ can be expressed as:
:<nowiki>$\begin {cases}
X = x - \dfrac {y' \paren {x'^2 + y'^2} } {x' y'' - y' x''} \\
Y = y + \dfrac {x' \paren {x'^2 + y'^2} } {x' y'' - y' x''}
\end {cases}$</nowiki>
where:
:$\tuple {x, y}$ denotes the Cartesian coordinates of a general point on $C$
:$\tuple {X, Y}$ denotes the Cartesian coordinates of a general point on the evolute of $C$
:$x'$ and $x' '$ denote the derivative and second derivative respectively of $x$ {{WRT|Differentiation}} $t$
:$y'$ and $y' '$ denote the derivative and second derivative respectively of $y$ {{WRT|Differentiation}} $t$.

Proof:
:400px
Let $P = \tuple {x, y}$ be a general point on $C$.
Let $Q = \tuple {X, Y}$ be the center of curvature of $C$ at $P$.
From the above diagram:
{{begin-eqn}}
{{eqn | l = x - X
      | r = \pm \rho \sin \psi
}}
{{eqn | l = Y - y
      | r = \pm \rho \cos \psi
}}
{{end-eqn}}
where:
:$\rho$ is the radius of curvature of $C$ at $P$
:$\psi$ is the angle between the tangent to $C$ at $P$ and the $x$-axis.
Whether the sign is plus or minus depends on whether the curve is convex or concave.
By definition of radius of curvature:
:$(1): \quad \begin {cases} x - X = \dfrac 1 k \sin \psi \\ Y - y = \dfrac 1 k \cos \psi \end {cases}$
where $k$ is the curvature of $C$ at $P$, given by:
:$k = \dfrac {x' y' ' - y' x' '} {\paren {x'^2 + y'^2}^{3/2} }$
We have that:
{{begin-eqn}}
{{eqn | l = \sin \psi
      | r = \dfrac {\d y} {\d s} = \dfrac {y'} {\sqrt {x'^2 + y'^2} }
}}
{{eqn | l = \cos \psi
      | r = \dfrac {\d x} {\d s} = \dfrac {x'} {\sqrt {x'^2 + y'^2} }
}}
{{end-eqn}}
Substituting for $k$ and $\psi$ in $(1)$ gives:
{{begin-eqn}}
{{eqn | l = x - X
      | r = \dfrac {\paren {x'^2 + y'^2}^{3/2} } {x' y' ' - y' x' '} \dfrac {y'} {\sqrt {x'^2 + y'^2} }
      | c = 
}}
{{eqn | r = \dfrac {y' \paren {x'^2 + y'^2} } {x' y' ' - y' x' '}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = X
      | r = x - \dfrac {y' \paren {x'^2 + y'^2} } {x' y' ' - y' x' '}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = Y - y
      | r = \dfrac {\paren {x'^2 + y'^2}^{3/2} } {x' y' ' - y' x' '} \dfrac {x'} {\sqrt {x'^2 + y'^2} }
      | c = 
}}
{{eqn | r = \dfrac {x' \paren {x'^2 + y'^2} } {x' y' ' - y' x' '}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = Y
      | r = y + \dfrac {x' \paren {x'^2 + y'^2} } {x' y' ' - y' x' '}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Evolute of Parabola

The evolute of the parabola $y = x^2$ is the curve:
:$27 X^2 = 16 \paren {Y - \dfrac 1 2}^3$

Proof:
From Parametric Equations for Evolute: Formulation 1:
:<nowiki>$\begin {cases}
X = x - \dfrac {y' \paren {1 + y'^2} } {y' '} \\
Y = y + \dfrac {1 + y'^2} {y''}
\end{cases}$</nowiki>
where:
:$\tuple {x, y}$ denotes the Cartesian coordinates of a general point on $C$
:$\tuple {X, Y}$ denotes the Cartesian coordinates of a general point on the evolute of $C$
:$y'$ and $y' '$ denote the derivative and second derivative respectively of $y$ {{WRT|Differentiation}} $x$.
Thus we have:
{{begin-eqn}}
{{eqn | l = y'
      | r = 2 x
      | c = 
}}
{{eqn | l = y' '
      | r = 2
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = X
      | r = x - \dfrac {2 x \paren {1 + \paren {2 x}^2} } 2
      | c = 
}}
{{eqn | r = x - x - 4 x^3
      | c = 
}}
{{eqn | r = -4 x^3
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = Y
      | r = x^2 + \dfrac {1 + \paren {2 x}^2} 2
      | c = 
}}
{{eqn | r = \frac {2 x^2 + 1 + 4 x^2} 2
      | c = 
}}
{{eqn | r = \frac {6 x^2 + 1} 2
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = Y
      | r = \frac {6 \paren {-\frac X 4}^{2/3} + 1} 2
      | c = substituting for $X$
}}
{{eqn | l = Y
      | r = 3 \paren {-\frac X 4}^{2/3} + \frac 1 2
      | c = substituting for $X$
}}
{{eqn | ll= \leadsto
      | l = \frac 1 3 \paren {Y - \frac 1 2}
      | r = \paren {\frac {X^2} {16} }^{1/3}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 27 X^2
      | r = 16 \paren {Y - \dfrac 1 2}^3
      | c = 
}}
{{end-eqn}}
The parabola (blue) and its evolute (red) are illustrated below:
400px
{{qed}}