Theorem: Ratio between Consecutive Highly Composite Numbers Greater than 2520 is Less than 2

The ratio between $2$ consecutive highly composite numbers both greater than $2520$ is less than $2$.

Proof:
{{AimForCont}} $n$ and $m$ are consecutive highly composite numbers such that:
:$2520 < n < m$
:$m / n \ge 2$
By definition of highly composite:
:$\map \tau m > \map \tau n$
and, {{hypothesis}}, $m$ is the smallest such integer.
We have that:
:$\map \tau {2 n} > \map \tau n$
so it follows that $m \le 2 n$, otherwise $m$ would ''not'' be the smallest such integer.
So from $m / n \ge 2$ and $m \le 2 n$, it follows that $m = 2 n$.
We have that $2520$ is a special highly composite number.
The prime decomposition of $2520$ s given by:
:$2520 = 2^3 \times 3^2 \times 5 \times 7$
We have that $n$ is a highly composite number such that $n > 2520$.
As $2520$ is a special highly composite number, $2520$ is a divisor of $n$.
Thus $n$ can be expressed as:
:$n = 2^a \times 3^b \times 5^c \times 7^d \times 11^e \times 13^f \times r$
where:
:$a \ge 3$
:$b \ge 2$
:$c \ge 1$
:$d \ge 1$
:$r$ is a possibly vacuous product of prime numbers strictly greater than $13$.
We have that $n$ and $m = 2 n$ are consecutive highly composite numbers.
Hence it follows that:
:$\map \tau {3 n / 2} \le \map \tau n$
and:
:$\map \tau {4 n / 3} \le \map \tau n$
otherwise $3 n / 2$ or $4 n / 3$ would be highly composite numbers between $n$ and $2 n$.
Then:
{{begin-eqn}}
{{eqn | l = \map \tau {3 n / 2}
      | o = \le
      | r = \map \tau n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^{a - 1} \times 3^{b + 1} \times 5^c \times 7^d \times 11^e \times 13^f \times r}
      | o = \le
      | r = \map \tau {2^a \times 3^b \times 5^c \times 7^d \times 11^e \times 13^f \times r}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^{a - 1} \times 3^{b + 1} } \times \map \tau {5^c \times 7^d \times 11^e \times 13^f \times r}
      | o = \le
      | r = \map \tau {2^a \times 3^b} \times \map \tau {5^c \times 7^d \times 11^e \times 13^f \times r}
      | c = Divisor Count Function is Multiplicative
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^{a - 1} \times 3^{b + 1} }
      | o = \le
      | r = \map \tau {2^a \times 3^b}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \paren {\paren {a - 1} + 1} \paren {\paren {b + 1} + 1}
      | o = \le
      | r = \paren {a + 1} \paren {b + 1}
      | c = {{Defof|Divisor Count Function}}
}}
{{eqn | ll= \leadsto
      | l = a \paren {b + 2}
      | o = \le
      | r = \paren {a + 1} \paren {b + 1}
      | c = simplifying
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map \tau {4 n / 3}
      | o = \le
      | r = \map \tau n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^{a + 2} \times 3^{b - 1} \times 5^c \times 7^d \times 11^e \times 13^f \times r}
      | o = \le
      | r = \map \tau {2^a \times 3^b \times 5^c \times 7^d \times 11^e \times 13^f \times r}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^{a + 2} \times 3^{b - 1} } \times \map \tau {5^c \times 7^d \times 11^e \times 13^f \times r}
      | o = \le
      | r = \map \tau {2^a \times 3^b} \times \map \tau {5^c \times 7^d \times 11^e \times 13^f \times r}
      | c = Divisor Count Function is Multiplicative
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^{a + 2} \times 3^{b - 1} }
      | o = \le
      | r = \map \tau {2^a \times 3^b}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \paren {\paren {a + 2} + 1} \paren {\paren {b - 1} + 1}
      | o = \le
      | r = \paren {a + 1} \paren {b + 1}
      | c = {{Defof|Divisor Count Function}}
}}
{{eqn | ll= \leadsto
      | l = \paren {a + 3} b
      | o = \le
      | r = \paren {a + 1} \paren {b + 1}
      | c = simplifying
}}
{{end-eqn}}
This leads to:
{{begin-eqn}}
{{eqn | l = a
      | o = \le
      | r = b + 1
      | c = 
}}
{{eqn | l = 2 b - 1
      | o = \le
      | r = a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 b - 1
      | o = \le
      | r = b + 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b
      | o = \le
      | r = 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | o = \le
      | r = 3
      | c = 
}}
{{end-eqn}}
It has already been established that:
:$a \ge 3$
:$b \ge 2$
{{begin-eqn}}
{{eqn | l = a
      | o = \ge
      | r = 3
}}
{{eqn | l = b
      | o = \le
      | r = 2
}}
{{end-eqn}}
so it is now possible to state:
{{begin-eqn}}
{{eqn | l = a
      | r = 3
}}
{{eqn | l = b
      | r = 2
}}
{{end-eqn}}
Suppose:
:$(1): \quad f \ge 1$
Then:
{{begin-eqn}}
{{eqn | l = 2^5 \times 3^3 \times 5^c \times 7^d \times 11^e \times 13^{f - 1} \times r
      | o = <
      | r = 2^3 \times 3^2 \times 5^c \times 7^d \times 11^e \times 13^f \times r
      | c = because $12 = 2^2 \times 3 < 13$
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^5 \times 3^3 \times 5^c \times 7^d \times 11^e \times 13^{f - 1} \times r}
      | o = <
      | r = \map \tau {2^3 \times 3^2 \times 5^c \times 7^d \times 11^e \times 13^f \times r}
      | c = as $2^3 \times 3^2 \times 5^c \times 7^d \times 11^e \times 13^f \times r$ is highly composite
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^5 \times 3^3 \times 13^{f - 1} } \times \map \tau {5^c \times 7^d \times 11^e \times r}
      | o = <
      | r = \map \tau {2^3 \times 3^2 \times 13^f} \times \map \tau {5^c \times 7^d \times 11^e \times r}
      | c = Divisor Count Function is Multiplicative
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^5 \times 3^3 \times 13^{f - 1} }
      | o = <
      | r = \map \tau {2^3 \times 3^2 \times 13^f}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \paren {5 + 1} \paren {3 + 1} \paren {\paren {f - 1} + 1}
      | o = <
      | r = \paren {3 + 1} \paren {2 + 1} \paren {f + 1}
      | c = {{Defof|Divisor Count Function}}
}}
{{eqn | ll= \leadsto
      | l = 24 f
      | o = <
      | r = 12 \paren {f + 1}
      | c = {{Defof|Divisor Count Function}}
}}
{{eqn | ll= \leadsto
      | l = f
      | o = <
      | r = 1
      | c = which is a contradiction of $(1)$
}}
{{end-eqn}}
So $f = 0$ and so by Prime Decomposition of Highly Composite Number $r = 1$.
Thus:
:$n = 2^3 \times 3^2 \times 5^c \times 7^d \times 11^e$
where $c = 1$ or $c = 2$.
Suppose $c = 2$.
Then:
{{begin-eqn}}
{{eqn | l = 2^5 \times 3^2 \times 5 \times 7^d \times 11^e
      | o = <
      | r = 2^3 \times 3^2 \times 5^2 \times 7^d \times 11^e
      | c = because $4 = 2^2 < 5$
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^5 \times 3^2 \times 5 \times 7^d \times 11^e}
      | o = <
      | r = \map \tau {2^3 \times 3^2 \times 5^2 \times 7^d \times 11^e}
      | c = as $2^3 \times 3^2 \times 5^2 \times 7^d \times 11^e$ is highly composite
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^5 \times 5} \times \map \tau {3^2 \times 7^d \times 11^e}
      | o = <
      | r = \map \tau {2^3 \times 5^2} \times \map \tau {3^2 \times 7^d \times 11^e}
      | c = Divisor Count Function is Multiplicative
}}
{{eqn | ll= \leadsto
      | l = \map \tau {2^5 \times 5}
      | o = <
      | r = \map \tau {2^3 \times 5^2}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \paren {5 + 1} \paren {1 + 1}
      | o = <
      | r = \paren {3 + 1} \paren {2 + 1}
      | c = {{Defof|Divisor Count Function}}
}}
{{eqn | ll= \leadsto
      | l = 12
      | o = <
      | r = 12
      | c = which is an absurdity
}}
{{end-eqn}}
So $c = 1$ and so by Prime Decomposition of Highly Composite Number:
:$n = 2^3 \times 3^2 \times 5 \times 7$
or:
:$n = 2^3 \times 3^2 \times 5 \times 7 \times 11$
Thus it has been established that these are the only possible values of $n$ greater than $2520$ which may fit the criteria for $n$ and $2 n$ to be consecutive highly composite numbers.
But the first of these is $2^3 \times 3^2 \times 5 \times 7 = 2520$ which fails through not being greater than $2520$.
Thus we consider:
:$n = 2^3 \times 3^2 \times 5 \times 7 \times 11 = 27 \, 720$
We have that:
{{begin-eqn}}
{{eqn | l = \map \tau {27 \, 720}
      | r = \map \tau {2^3 \times 3^2 \times 5 \times 7 \times 11}
      | c = 
}}
{{eqn | r = \paren {3 + 1} \paren {2 + 1} \paren {1 + 1} \paren {1 + 1} \paren {1 + 1}
      | c = 
}}
{{eqn | r = 96
      | c = 
}}
{{end-eqn}}
It is now necessary to show that there are no highly composite numbers between $27 \, 720$ and $2 \times 27 \, 720 = 55 \, 440$.
That is, all numbers $n$ such that $27 \, 720 < n < 55 \, 440$ are to be shown to have $\map \tau n < 96$.
But:
{{begin-eqn}}
{{eqn | l = \map \tau {45 \, 360}
      | r = \map \tau {2^4 \times 3^4 \times 5 \times 7}
      | c = 
}}
{{eqn | r = \paren {4 + 1} \paren {4 + 1} \paren {1 + 1} \paren {1 + 1}
      | c = 
}}
{{eqn | r = 100
      | c = 
}}
{{end-eqn}}
So $45 \, 360$ has a higher $\tau$ than $27 \, 720$ and so the next higher highly composite number than $27 \, 720$ is less than twice it.
The result follows by Proof by Contradiction.
{{qed}}