Strictly increasing completely multiplicative functions are powers $n^\alpha$

Proved

HardyFiveAxioms.strictMono_completelyMultiplicative_eq_rpow

by Lucas · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsnumber-theoryquantum-foundations

Let $K$ be a real-valued function on the positive integers that is strictly increasing ( $K(m)<K(n)$ whenever $1\le m<n$ ) and completely multiplicative ( $K(mn)=K(m)K(n)$ for all $m,n\ge1$ ). Then there is a real $\alpha>0$ such that

K(n)=n^\alpha\qquad\text{for all }n\ge1 .

This is the number-theoretic input of Hardy's proof that $K=N^r$ .

Formalization Note $K$ is a function ℕ → ℝ, constrained only on arguments $\ge1$ , and $n^\alpha$ is the real power Real.rpow. The paper notes $\alpha>0$ in the course of the proof, and the statement includes it in the conclusion.

Preamble

import Mathlib

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Appendix 2: a strictly increasing, completely multiplicative function on the
positive integers is of the form `K(n) = n^α` (with `α > 0`). -/
theorem strictMono_completelyMultiplicative_eq_rpow (K : ℕ → ℝ)
    (hmono : ∀ m n : ℕ, 1 ≤ m → m < n → K m < K n)
    (hmul : ∀ m n : ℕ, 1 ≤ m → 1 ≤ n → K (m * n) = K m * K n) :
    ∃ α : ℝ, 0 < α ∧ ∀ n : ℕ, 1 ≤ n → K n = (n : ℝ) ^ α := by sorry

end HardyFiveAxioms

Source

L. Hardy, *Quantum Theory From Five Reasonable Axioms*, arXiv:quant-ph/0101012v4 (2001), https://arxiv.org/abs/quant-ph/0101012, pp. 29–30, Appendix 2, Eqs. (118)–(128)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may share the drafter's blind spots. Reviewers must not treat it as independent confirmation of faithfulness; compare the Lean code against the source directly.

Let $K:\mathbb N\to\mathbb R$ be any function. Assume:

for all natural numbers $m,n$ with $1\le m$ and $m<n$ : $K(m)<K(n)$ ;
for all natural numbers $m\ge1$ , $n\ge1$ : $K(mn)=K(m)K(n)$ .

Then there is a real number $\alpha$ with $\alpha>0$ such that $K(n)=n^\alpha$ for every natural number $n\ge1$ . Here $n^\alpha$ is the real power of the positive real $n$ , i.e. $e^{\alpha\ln n}$ . The value $K(0)$ is unconstrained.

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Strictly increasing completely multiplicative functions are powers nαn^\alphanα

Strictly increasing completely multiplicative functions are powers $n^\alpha$