log_ratio
plain-language theorem explainer
For a nondecreasing completely multiplicative f : ℕ → ℝ with f(2) > 1, the cross-multiplied log ratios agree: log(f n)·log 2 = log(f 2)·log n for every n ≥ 2. Anyone proving that such an f is a pure power cites this identity. The argument squeezes n^k between consecutive powers of two, transfers the squeeze through f and logs, then lets k grow to force the difference to vanish.
Claim. Let $f:\mathbb{N}\to\mathbb{R}$ be completely multiplicative and nondecreasing on the positive integers, with $f(1)=1$ and $f(2)>1$. Then for every integer $n\ge 2$, $$\log(f(n))\cdot\log 2 = \log(f(2))\cdot\log n.$$
background
The ambient structure is a completely multiplicative nondecreasing map $f:\mathbb{N}\to\mathbb{R}$: $f(1)=1$, $f(mn)=f(m)f(n)$ whenever $m,n\ge 1$, and $m\le n$ (with $m\ge 1$) implies $f(m)\le f(n)$. Values at $0$ are unconstrained. Complete multiplicativity on pure powers is packaged as $f(m^j)=f(m)^j$ for $m\ge 1$.
The module develops Howe's route to the completely multiplicative case of Erdős's theorem on monotone multiplicative functions: such an $f$ must be a pure power $n\mapsto n^c$ for a single nonnegative real $c$. The present identity is the quantitative heart of that argument. It equates the logarithmic growth rates of $f$ at every base $n\ge 2$ with the rate at base two, written cross-multiplied so that no division by logs appears.
Positivity of the four logs in play follows from $f(2)>1$ together with monotonicity (which forces $f(n)>1$) and the elementary bound $n\ge 2$.
proof idea
Introduce abbreviations $L_2=\log 2$, $L_n=\log n$, $M_2=\log(f 2)$, $M_n=\log(f n)$ and record that all four are positive. The key estimate is: for every $k\ge 1$, $$k,|M_n L_2-M_2 L_n|\le M_2 L_2.$$
To prove it, set $j=\mathrm{Nat.log},2,(n^k)$, so $2^j\le n^k<2^{j+1}$. Pass to reals and take logs to sandwich $k L_n$ between $j L_2$ and $(j+1)L_2$. Apply monotonicity of $f$ to the same integer bounds, rewrite via the power identity $f(m^j)=f(m)^j$, and take logs again to sandwich $k M_n$ between $j M_2$ and $(j+1)M_2$. Four multiplications by the positive quantities $L_2$ and $M_2$, followed by nlinarith on the absolute value, yield the key bound.
Conclude by contradiction: if $M_n L_2\ne M_2 L_n$, the absolute difference is positive; choose $k$ larger than $(M_2 L_2)/|\cdots|$ and compare the key bound at $k+1$ to obtain an immediate numerical contradiction.
why it matters
This identity is the engine of exists_exponent, the completely multiplicative case of Erdős's theorem in Howe's form: a nondecreasing completely multiplicative $f$ is $n\mapsto n^c$ for a unique $c\ge 0$ (with the constant function $1$ corresponding to $c=0$). The parent theorem splits on whether $f(2)=1$ or $f(2)>1$; in the nondegenerate branch it invokes the present cross-multiplication to define $c=\log(f 2)/\log 2$ and verify $f(n)=n^c$ for all $n\ge 1$.
In the Recognition cost ledger, completely multiplicative monotone characters are the natural candidates for cost-preserving maps on the positive integers. Forcing them to be pure powers pins the admissible cost growth to a single real exponent, which is the arithmetic input needed when cost data are later matched to the $\varphi$-ladder and the J-cost fixed-point structure (T5–T6). The sibling monotoneMultiplicative_id records that the identity map itself is such a character (exponent one), giving the baseline against which other exponents are compared.
No scaffolding remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.