avewright/proofwiki-math huggingface dataset:
Theorem: Lower Closure of Meet of Lower Closures

Let $\struct {S, \preceq}$ be a meet semilattice.
Let $D_1, D_2$ be subsets of $S$.
Then:
:$\set {i_1 \wedge i_2: i_1 \in D_1^\preceq, i_2 \in D_2^\preceq}^\preceq = \set {i_1 \wedge i_2: i_1 \in D_1, i_2 \in D_2}^\preceq$
where
:$D_1^\preceq$ denotes the lower closure of $D_1$.

Proof:
By Lower Closure is Closure Operator:
:$D_1 \subseteq D_1^\preceq$ and $D_2 \subseteq D_2^\preceq$
Then
:$\set {i_1 \wedge i_2: i_1 \in D_1, i_2 \in D_2} \subseteq \set {i_1 \wedge i_2: i_1 \in D_1^\preceq, i_2 \in D_2^\preceq}$
By Lower Closure is Closure Operator:
:$\set {i_1 \wedge i_2: i_1 \in D_1, i_2 \in D_2}^\preceq \subseteq \set {i_1 \wedge i_2: i_1 \in D_1^\preceq, i_2 \in D_2^\preceq}^\preceq$
By definition of set equality it remains to prove that
:$\set {i_1 \wedge i_2: i_1 \in D_1^\preceq, i_2 \in D_2^\preceq}^\preceq \subseteq \set {i_1 \wedge i_2: i_1 \in D_1, i_2 \in D_2}^\preceq$
Let $x \in \set {i_1 \wedge i_2: i_1 \in D_1^\preceq, i_2 \in D_2^\preceq}^\preceq$.
By definition of lower closure of set:
:$\exists y \in \set {i_1 \wedge i_2: i_1 \in D_1^\preceq, i_2 \in D_2^\preceq} \land x \preceq y$
Then:
:$\exists i_1 \in D_1^\preceq, i_2 \in D_2^\preceq: y = i_1 \wedge i_2$
By definition of lower closure of set:
:$\exists d_1 \in D_1: i_1 \preceq d_1$
and
:$\exists d_2 \in D_2: i_2 \preceq d_2$
By Meet Semilattice is Ordered Structure:
:$y \preceq d_1 \wedge d_2$
By definition of transitivity:
:$x \preceq d_1 \wedge d_2$
:$d_1 \wedge d_2 \in \set {i_1 \wedge i_2: i_1 \in D_1, i_2 \in D_2}$
Thus by definition of lower closure of set:
:$x \in \set {i_1 \wedge i_2: i_1 \in D_1, i_2 \in D_2}^\preceq$
Thus the result.
{{qed}}
Theorem: Equation of Cycloid in Cartesian Coordinates

Consider a circle of radius $a$ rolling without slipping along the $x$-axis of a cartesian plane.
Consider the point $P$ on the circumference of this circle which is at the origin when its center is on the y-axis.
Consider the cycloid 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 equation:
:$a \sin^{-1} \paren {\dfrac {\sqrt {2 a y - y^2} } a} = \sqrt {2 a y - y^2} + x$

Proof:
From Equation of Cycloid, the point $P = \tuple {x, y}$ is described by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
Expressing $\theta$ and $\sin \theta$ in terms of $y$:
{{begin-eqn}}
{{eqn | l = \cos \theta
      | r = 1 - \frac y a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sin \theta
      | r = \sqrt {1 - \paren {1 - \frac y a}^2}
      | c = 
}}
{{eqn | r = \sqrt {\frac {2 y} a - \frac {y^2} {a^2} }
      | c = 
}}
{{eqn | r = \frac {\sqrt {2 a y - y^2} } a 
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \theta
      | r = \sin^{-1} \paren {\frac {\sqrt {2 a y - y^2} } a}
      | c = 
}}
{{end-eqn}}
Substituting for $\theta$ and $\sin \theta$ in the expression for $x$:
{{begin-eqn}}
{{eqn | l = x
      | r = a \paren {\sin^{-1} \paren {\frac {\sqrt {2 a y - y^2} } a} - \frac 1 a \sqrt {2 a y - y^2} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a \sin^{-1} \paren {\frac {\sqrt {2 a y - y^2} } a}
      | r = \sqrt {2 a y - y^2} + x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Second Derivative of Locus of Cycloid

Consider a circle of radius $a$ rolling without slipping along the x-axis of a cartesian plane.
Consider the point $P$ on the circumference of this circle which is at the origin when its center is on the y-axis.
Consider the cycloid traced out by the point $P$.
Let $\tuple {x, y}$ be the coordinates of $P$ as it travels over the plane.
The second derivative of the locus of $P$ is given by:
:$y' ' = -\dfrac a {y^2}$

Proof:
From Equation of Cycloid:
{{begin-eqn}}
{{eqn | l = x
      | r = a \paren {\theta - \sin \theta}
}}
{{eqn | l = y
      | r = a \paren {1 - \cos \theta}
}}
{{end-eqn}}
From Slope of Tangent to Cycloid:
{{begin-eqn}}
{{eqn | l = y'
      | r = \cot \dfrac \theta 2
      | c = Slope of Tangent to Cycloid
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d y'} {\d x}
      | r = \dfrac {\d} {\d \theta} \cot \dfrac \theta 2 \frac {\d \theta} {\d x}
      | c = Chain Rule for Derivatives
}}
{{eqn | r = -\dfrac 1 2 \csc^2 \dfrac \theta 2 / \dfrac {\d x} {\d \theta}
      | c = Derivative of Cotangent Function
}}
{{eqn | r = -\dfrac 1 2 \csc^2 \dfrac \theta 2 \paren {\dfrac 1 {a \paren {1 - \cos \theta} } }
      | c = Derivative of Sine Function
}}
{{eqn | r = -\dfrac 1 {2 \sin^2 \dfrac \theta 2} \paren {\dfrac 1 {a \paren {1 - \cos \theta} } }
      | c = {{Defof|Cosecant}}
}}
{{eqn | r = -\dfrac 1 {1 - \cos \theta} \paren {\dfrac 1 {a \paren {1 - \cos \theta} } }
      | c = {{Corollary|Double Angle Formula for Cosine|5}}
}}
{{eqn | r = -\dfrac a {y^2}
      | c = from $y = a \paren {1 - \cos \theta}$
}}
{{end-eqn}}
{{qed}}
Theorem: Arc of Cycloid is Concave

Consider a circle of radius $a$ rolling without slipping along the x-axis of a cartesian plane.
Consider the point $P$ on the circumference of this circle which is at the origin when its center is on the y-axis.
Consider the cycloid traced out by the point $P$.
Let $\tuple {x, y}$ be the coordinates of $P$ as it travels over the plane.
Then the locus of $P$ is concave.

Proof:
From Second Derivative of Locus of Cycloid:
:$y' ' = -\dfrac a {y^2}$
As $y \ge 0$ throughout, then $y' ' < 0$ wherever $y \ne 0$, which is at the cusps.
The result follows from Second Derivative of Concave Real Function is Non-Positive.
{{qed}}
Theorem: Normal to Cycloid passes through Bottom of Generating Circle

Let $C$ be a cycloid generated by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
Then the normal to $C$ at a point $P$ on $C$ passes through the bottom of the generating circle of $C$.

Proof:
From Normal to Cycloid, the equation for the normal to $C$ at a point $P = \tuple {x, y}$ is given by:
{{ProofWanted|We don't even have the definition of a normal to a curve posted up yet, so there's a long way to go here.}}
Theorem: Normal to Cycloid passes through Bottom of Generating Circle

Let $C$ be a cycloid generated by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
Then the normal to $C$ at a point $P$ on $C$ passes through the bottom of the generating circle of $C$.

Proof:
From Tangent to Cycloid passes through Top of Generating Circle, the tangent to $C$ at a point $P = \tuple {x, y}$ passes through the top of the generating circle.
By definition, the normal to $C$ at $P$ is perpendicular to the tangent to $C$ at $P$.
From Thales' Theorem, the normal, the tangent and the diameter of the generating circle form a right triangle.
Thus the normal to $C$ at $P$ meets the generating circle at the opposite end of the diameter to the tangent.
Hence the result.
{{qed}}
Theorem: Rate of Change of Cartesian Coordinates of Cycloid

Let a circle $C$ of radius $a$ roll without slipping along the x-axis of a cartesian plane at a constant speed such that the center moves with a velocity $\mathbf v_0$ in the direction of increasing $x$.
Consider a point $P$ on the circumference of this circle.
Let $\tuple {x, y}$ be the coordinates of $P$ as it travels over the plane.
Then the rate of change of $x$ and $y$ can be expresssed as:
{{begin-eqn}}
{{eqn | l = \frac {\d x} {\d t}
      | r = \mathbf v_0 \paren {1 - \cos \theta}
      | c = 
}}
{{eqn | l = \frac {\d y} {\d t}
      | r = \mathbf v_0 \sin \theta
      | c = 
}}
{{end-eqn}}
where $\theta$ is the angle turned by $C$ after time $t$.

Proof:
Let the center of $C$ be $O$.
{{WLOG}}, let $P$ be at the origin at time $t = t_0$.
By definition, $P$ traces out a cycloid.
From Equation of Cycloid, the point $P = \tuple {x, y}$ is described by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
Let $\tuple {x_c, y_c}$ be the coordinates of $O$ at time $t$.
We have that:
:$y_c$ is constant: $y_c = a$
From Equations of Motion with Constant Acceleration: Velocity after Time
:$x_c = \mathbf v_0 t$
as the acceleration of $O$ is zero.
But $x_c$ is equal to the length of the arc of $C$ that has rolled along the $x$-axis.
By Arc Length of Sector:
:$x_c = a \theta$
and so:
{{begin-eqn}}
{{eqn | n = 1
      | l = \theta
      | r = \frac {\mathbf v_0 t} a
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \frac {\d \theta} {\d t}
      | r = \frac {\mathbf v_0} a
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = x
      | r = a \paren {\frac {\mathbf v_0 t} a - \sin \theta}
      | c = substituting for $\theta$ from $(1)$
}}
{{eqn | l = x
      | r = \mathbf v_0 t - a \sin \theta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d t}
      | r = \mathbf v_0 - a \cos \theta \frac {\d \theta} {\d t}
      | c = Chain Rule for Derivatives and Derivative of Sine Function
}}
{{eqn | r = \mathbf v_0 - a \cos \theta \frac {\mathbf v_0} a
      | c = from $(2)$
}}
{{eqn | r = \mathbf v_0 \paren {1 - \cos \theta}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = y
      | r = a \paren {1 - \cos \theta}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d t}
      | r = a \sin \theta \frac {\d \theta} {\d t}
      | c = Chain Rule for Derivatives and Derivative of Cosine Function
}}
{{eqn | r = a \sin \theta \frac {\mathbf v_0} a
      | c = from $(2)$
}}
{{eqn | r = \mathbf v_0 \sin \theta
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Maximum Rate of Change of X Coordinate of Cycloid

Let a circle $C$ of radius $a$ roll without slipping along the x-axis of a cartesian plane at a constant speed such that the center moves with a velocity $\mathbf v_0$ in the direction of increasing $x$.
Consider a point $P$ on the circumference of this circle.
Let $\tuple {x, y}$ be the coordinates of $P$ as it travels over the plane.
The maximum rate of change of $x$ is $2 \mathbf v_0$, which happens when $P$ is at the top of the circle $C$.

Proof:
From Rate of Change of Cartesian Coordinates of Cycloid, the rate of change of $x$ is given by:
:$\dfrac {\d x} {\d t} = \mathbf v_0 \paren {1 - \cos \theta}$
This is a maximum when $1 - \cos \theta$ is a maximum.
That happens when $\cos \theta$ is at a minimum.
That happens when $\cos \theta = -1$.
That happens when $\theta = \pi, 3 \pi, \ldots$
That is, when $\theta = \paren {2 n + 1} \pi$ where $n \in \Z$.
That is, when $P$ is at the top of the circle $C$.
When $\cos \theta = -1$ we have:
{{begin-eqn}}
{{eqn | l = \frac {\d x} {\d t}
      | r = \mathbf v_0 \paren {1 - \paren {-1} }
      | c = 
}}
{{eqn | r = 2 \mathbf v_0
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Maximum Rate of Change of Y Coordinate of Cycloid

Let a circle $C$ of radius $a$ roll without slipping along the x-axis of a cartesian plane at a constant speed such that the center moves with a velocity $\mathbf v_0$ in the direction of increasing $x$.
Consider a point $P$ on the circumference of this circle.
Let $\tuple {x, y}$ be the coordinates of $P$ as it travels over the plane.
The maximum rate of change of $y$ is $\mathbf v_0$, which happens when $\theta = \dfrac \pi 2 + 2 n \pi$ where $n \in \Z$.

Proof:
From Rate of Change of Cartesian Coordinates of Cycloid, the rate of change of $y$ is given by:
:$\dfrac {\d y} {\d t} = \mathbf v_0 \sin \theta$.
This is a maximum when $\sin \theta$ is a maximum.
That happens when $\sin \theta = 1$.
That happens when $\theta = \dfrac \pi 2 + 2 n \pi$ where $n \in \Z$.
When $\sin \theta = 1$ we have:
:$\dfrac {\d y} {\d t} = \mathbf v_0$
Hence the result.
{{qed}}
Theorem: Lower Closure is Closure Operator

Let $\struct {S, \preceq}$ be an ordered set.
Then
:lower closure of set is a closure operator.

Proof:
=== Inflationary ===
Let $X$ be a subset of $S$.
Let $x \in X$.
By definition of reflexivity:
:$x \preceq x$
Thus by definition of lower closure of set:
:$x \in X^\preceq$
Thus by definition of subset:
:$X \subseteq X^\preceq$
{{qed|lemma}}
Theorem: Area inside Astroid

The area inside an astroid $H$ constructed within a circle of radius $a$ is given by:
:$\AA = \dfrac {3 \pi a^2} 8$

Proof:
Let $H$ be embedded in a cartesian plane with its center at the origin and its cusps positioned on the axes.
:400px
By symmetry, it is sufficient to evaluate the area shaded yellow and to multiply it by $4$.
By Equation of Astroid:
:$\begin{cases}
x & = a \cos^3 \theta \\
y & = a \sin^3 \theta
\end{cases}$
Thus:
{{begin-eqn}}
{{eqn | l = \AA
      | r = 4 \int_0^a y \rd x
      | c = 
}}
{{eqn | r = 4 \int_{x \mathop = 0}^{x \mathop = a} y \frac {\d x} {\d \theta} \rd \theta
      | c = 
}}
{{eqn | r = 4 \int_{x \mathop = 0}^{x \mathop = a} a \sin^3 \theta \, 3 a \cos^2 \theta \paren {-\sin \theta} \rd \theta
      | c = differentiating $a \cos^3 \theta$ {{WRT|Differentiation}} $\theta$
}}
{{eqn | r = 4 \int_{\theta \mathop = \pi / 2}^{\theta \mathop = 0} a \sin^3 \theta \, 3 a \cos^2 \theta \paren {-\sin \theta} \rd \theta
      | c = $x = 0$ when $\theta = \pi / 2$, $x = a$ when $\theta = 0$
}}
{{eqn | r = 12 a^2 \int_0^{\pi / 2} \sin^4 \theta \cos^2 \theta \rd \theta
      | c = simplifying
}}
{{end-eqn}}
Simplifying the integrand:
{{begin-eqn}}
{{eqn | l = \sin^4 \theta \cos^2 \theta
      | r = \frac {\paren {2 \sin \theta \cos \theta}^2} 4 \frac {2 \sin^2 \theta} 2
      | c = 
}}
{{eqn | r = \frac {\sin^2 2 \theta} 4 \frac {2 \sin^2 \theta} 2
      | c = Double Angle Formula for Sine
}}
{{eqn | r = \frac {\sin^2 2 \theta} 4 \frac {1 - \cos 2 \theta} 2
      | c = Square of Sine
}}
{{eqn | r = \frac {\sin^2 2 \theta - \sin^2 2 \theta \cos 2 \theta} 8
      | c = 
}}
{{eqn | r = \frac {1 - \cos 4 \theta} {16} - \frac {\sin^2 2 \theta \cos 2 \theta} 8
      | c = Square of Sine
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \AA
      | r = 12 a^2 \int_0^{\pi / 2} \paren {\frac {1 - \cos 4 \theta} {16} - \frac {\sin^2 2 \theta \cos 2 \theta} 8} \rd \theta
      | c = 
}}
{{eqn | r = \frac 3 4 a^2 \int_0^{\pi / 2} \paren {1 - \cos 4 \theta} \rd \theta - \frac 3 2 a^2 \int_0^{\pi / 2} \sin^2 2 \theta \cos 2 \theta \rd \theta
      | c = Linear Combination of Definite Integrals
}}
{{eqn | r = \frac 3 4 a^2 \intlimits {\theta - \frac {\sin 4 \theta} 4} 0 {\pi / 2} - \frac 3 2 a^2 \int_0^{\pi / 2} \sin^2 2 \theta \cos 2 \theta \rd \theta
      | c = Primitive of $\cos a x$
}}
{{eqn | r = \frac 3 4 a^2 \intlimits {\theta - \frac {\sin 4 \theta} 4} 0 {\pi / 2} - \frac 3 2 a^2 \intlimits {\frac {\sin^3 2 \theta} 6} 0 {\pi / 2}
      | c = Primitive of $\sin^n a x \cos a x$
}}
{{eqn | r = \frac {3 \pi a^2} 8 - \frac {3 a^2} {16} \sin 2 \pi  - \frac {3 a^2} {12} \sin^3 \pi
      | c = evaluating limits of integration
}}
{{eqn | r = \frac {3 \pi a^2} 8
      | c = $\sin 2 \pi = 0$ and $\sin^3 \pi = 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Length of Arc of Astroid

The total length of the arcs of an astroid constructed within a deferent of radius $a$ is given by:
:$\LL = 6 a$

Proof:
Let $H$ be embedded in a cartesian plane with its center at the origin and its cusps positioned on the axes.
:400px
We have that $\LL$ is $4$ times the length of one arc of the astroid.
From Arc Length for Parametric Equations:
:$\ds \LL = 4 \int_{\theta \mathop = 0}^{\theta \mathop = \pi/2} \sqrt {\paren {\frac {\d x} {\d \theta} }^2 + \paren {\frac {\d y} {\d \theta} }^2} \rd \theta$
where, from Equation of Astroid:
:$\begin{cases} x & = a \cos^3 \theta \\ y & = a \sin^3 \theta \end{cases}$
We have:
{{begin-eqn}}
{{eqn | l = \frac {\d x} {\d \theta}
      | r = -3 a \cos^2 \theta \sin \theta
      | c = 
}}
{{eqn | l = \frac {\d y} {\d \theta}
      | r = 3 a \sin^2 \theta \cos \theta
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \sqrt {\paren {\frac {\d x} {\d \theta} }^2 + \paren {\frac {\d y} {\d \theta} }^2}
      | r = \sqrt {9 a^2 \paren {\sin^4 \theta \cos^2 \theta + \cos^4 \theta \sin^2 \theta} }
      | c = 
}}
{{eqn | r = 3 a \sqrt {\sin^2 \theta \cos^2 \theta \paren {\sin^2 \theta + \cos^2 \theta} }
      | c = 
}}
{{eqn | r = 3 a \sqrt {\sin^2 \theta \cos^2 \theta}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = 3 a \sin \theta \cos \theta
      | c = 
}}
{{eqn | r = \frac {3 a \sin 2 \theta} 2
      | c = Double Angle Formula for Sine
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \LL
      | r = 4 \frac {3 a} 2 \int_0^{\pi / 2} \sin 2 \theta \rd \theta
      | c = 
}}
{{eqn | r = 6 a \intlimits {\frac {-\cos 2 \theta} 2} 0 {\pi / 2}
      | c = Primitive of $\sin a x$
}}
{{eqn | r = 6 a \paren {-\frac {\cos \pi} 2 + \frac {\cos 0} 2}
      | c = evaluating limits of integration
}}
{{eqn | r = 6 a \frac {-\paren {-1} + 1} 2
      | c = 
}}
{{eqn | r = 6 a
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Area of Surface of Revolution from Astroid

Let $H$ be the astroid constructed within a circle of radius $a$.
The surface of revolution formed by rotating $H$ around the $x$-axis:
:400px
evaluates to:
:$\SS = \dfrac {12 \pi a^2} 5$

Proof:
By symmetry, it is sufficient to calculate the surface of revolution of $H$ for $0 \le x \le a$.
From Area of Surface of Revolution, this surface of revolution is given by:
:$\ds \SS = 2 \int_0^{\pi / 2} 2 \pi y \, \sqrt {\paren {\frac {\d x} {\d \theta} }^2 + \paren {\frac {\d y} {\d \theta} }^2} \rd \theta$
From Equation of Astroid:
:<nowiki>$\begin{cases}
x & = a \cos^3 \theta \\
y & = a \sin^3 \theta
\end{cases}$</nowiki>
so:
{{begin-eqn}}
{{eqn | l = \frac {\d x} {\d \theta}
      | r = -3 a \cos^2 \theta \sin \theta
      | c = 
}}
{{eqn | l = \frac {\d y} {\d \theta}
      | r = 3 a \sin^2 \theta \cos \theta
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \sqrt {\paren {\frac {\d x} {\d \theta} }^2 + \paren {\frac {\d y} {\d \theta} }^2}
      | r = \sqrt {9 a^2 \paren {\sin^4 \theta \cos^2 \theta + \cos^4 \theta \sin^2 \theta} }
      | c = 
}}
{{eqn | r = 3 a \sqrt {\sin^2 \theta \cos^2 \theta \paren {\sin^2 \theta + \cos^2 \theta} }
      | c = 
}}
{{eqn | r = 3 a \sqrt {\sin^2 \theta \cos^2 \theta}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = 3 a \sin \theta \cos \theta
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \SS
      | r = 2 \int_0^{\pi / 2} 2 \pi a \sin^3 \theta \, 3 a \sin \theta \cos \theta \rd \theta
      | c = 
}}
{{eqn | r = 12 \pi a^2 \int_0^{\pi / 2} \sin^4 \theta \cos \theta \rd \theta
      | c = 
}}
{{eqn | r = 12 \pi a^2 \intlimits {\frac {\sin^5 \theta} 5} 0 {\pi / 2}
      | c = Primitive of $\sin^n a x \cos a x$
}}
{{eqn | r = \frac {12 \pi a^2} 5 \paren {\sin^5 \theta \frac \pi 2 - \sin^5 \theta 0}
      | c = evaluating limits of integration
}}
{{eqn | r = \frac {12 \pi a^2} 5 \paren {1 - 0}
      | c = 
}}
{{eqn | r = \frac {12 \pi a^2} 5
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Tusi Couple is Diameter of Deferent

A Tusi couple is a degenerate case of the hypocycloid whose form is a straight line that forms a diameter of the deferent.

Proof:
Let $C_1$ be a circle of radius $b$ rolling without slipping around the inside 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 hypocycloid formed by the locus of $P$.
From Number of Cusps of Hypocycloid from Integral Ratio of Circle Radii we have that $H$ will have $2$ cusps {{iff}}:
:$a = 2 b$
By Equation of Hypocycloid a hypocycloid can be expressed in parametric form as:
:$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}$
Hence:
{{begin-eqn}}
{{eqn | l = x
      | r = \paren {2 b - b} \cos \theta + b \map \cos {\paren {\dfrac {2 b - b} b} \theta}
      | c = 
}}
{{eqn | r = b \cos \theta + b \cos \theta
      | c = 
}}
{{eqn | r = 2 b \cos \theta 
      | c = 
}}
{{end-eqn}}
Thus the $x$ coordinate of the $2$ cusp hypocycloid has a range $\closedint {-b} b$.
Similarly:
{{begin-eqn}}
{{eqn | l = y
      | r = \paren {2 b - b} \sin \theta - b \map \sin {\paren {\dfrac {2 b - b} b} \theta}
      | c = 
}}
{{eqn | r = b \sin \theta - b \sin \theta
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
Thus the $y$ coordinate of the $2$ cusp hypocycloid is fixed at $y = 0$.
Thus the $2$ cusp hypocycloid consists of the line segment:
:$x \in \closedint {-b} b, y = 0$.
which is a diameter of the containing circle.
{{qed}}
Theorem: Equation of Astroid/Parametric Form

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

Proof:
By definition, an astroid is a hypocycloid with $4$ cusps.
:400px
By Equation of Hypocycloid, the equation of $H$ is given by:
:<nowiki>$\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}$</nowiki>
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 4$ the radius of the deferent.
Thus $a = 4 b$ and the equation of $H$ is now given by:
:<nowiki>$\begin{cases}
x & = 3 b \cos \theta + b \cos 3 \theta \\
y & = 3 b \sin \theta - b \sin 3 \theta
\end{cases}$</nowiki>
From Triple Angle Formula for Cosine:
:$\cos 3 \theta = 4 \cos^3 \theta - 3 \cos \theta$
and from Triple Angle Formula for Sine:
:$\sin 3 \theta = 3 \sin \theta - 4 \sin^3 \theta$
Thus $H$ can be expressed as:
:<nowiki>$\begin{cases}
x & = 4 b \cos^3 \theta = a \cos^3 \theta \\
y & = 4 b \sin^3 \theta = a \sin^3 \theta
\end{cases}$</nowiki>
{{qed}}
Theorem: Equation of Astroid/Cartesian Form

The point $P = \tuple {x, y}$ is described by the equation:
:$x^{2/3} + y^{2/3} = a^{2/3}$

Proof:
By definition, an astroid is a hypocycloid with $4$ cusps.
:400px
From the parametric form of the equation of an astroid, $H$ can be expressed as:
:<nowiki>$\begin{cases}
x & = 4 b \cos^3 \theta = a \cos^3 \theta \\
y & = 4 b \sin^3 \theta = a \sin^3 \theta
\end{cases}$</nowiki>
Squaring, taking cube roots and adding:
{{begin-eqn}}
{{eqn | l = x^{2/3} + y^{2/3}
      | r = a^{2/3} \paren {\cos^2 \theta + \sin^2 \theta}
      | c = 
}}
{{eqn | r = a^{2/3}
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Preceding iff Meet equals Less Operand

Let $\struct {S, \preceq}$ be a meet semilattice.
Let $x, y \in S$.
Then
:$x \preceq y$ {{iff}} $x \wedge y = x$

Proof:
=== Sufficient Condition ===
Let
:$x \preceq y$
By definition of meet:
:$x \wedge y = \inf \set {x, y}$
By definitions of lower bound and reflexivity:
:$x$ is lower bound for $\set {x, y}$
and
:$\forall z \in S: z$ is lower bound for $\set {x, y} \implies z \preceq x$
Thus by definition of infimum:
:$x = \inf \set {x, y} = x \wedge y$
{{qed|lemma}}
Theorem: Simple Harmonic Motion of Point on Tusi Couple

Let $C_1$ and $C_2$ be the epicycle and deferent respectively of a Tusi couple $H$.
Let $C_2$ be embedded in a cartesian plane with its center $O$ located at the origin.
Let the center of $C_1$ move at a constant angular velocity $\omega$ around the center of $C_2$.
Let $P$ be the point on the circumference of $C_1$ whose locus is $H$.
Let $C_1$ be initially positioned so that $P$ its point of tangency to $C_2$, located on the $x$-axis.
Then $P$ moves back and forward on the $x$-axis with simple harmonic motion with period $\dfrac {2 \pi} \omega$ and maximum speed $a \omega$.

Proof:
{{ProofWanted|Straightforward but tedious. I'll get back to it in due course.}}