monotoneMultiplicative_id
plain-language theorem explainer
The natural embedding of the naturals into the reals is completely multiplicative and nondecreasing on positive integers. Anyone applying the Erdős–Howe power classification of such maps needs this as the canonical exponent-one instance. The proof is three short tactics: unit by arithmetic, multiplicativity by cast-and-ring, monotonicity by transporting the integer order.
Claim. The map $n \mapsto (n:\mathbb{R})$ from $\mathbb{N}$ to $\mathbb{R}$ satisfies $f(1)=1$, $f(mn)=f(m)f(n)$ for all integers $m,n\geq 1$, and $m\leq n$ (with $m\geq 1$) implies $f(m)\leq f(n)$.
background
A MonotoneMultiplicative map is a function $f:\mathbb{N}\to\mathbb{R}$ that is completely multiplicative and nondecreasing on the positive integers, normalized by $f(1)=1$. The value $f(0)$ is left free: the cost-ledger character has no content at zero.
The module's main theorem is exists_exponent (Erdős's theorem in the completely multiplicative case, via Howe's argument): every such $f$ is a pure power $f(n)=n^c$ for a single nonnegative real exponent $c$, with the constant function corresponding to $c=0$. The squeeze that forces a common log-ratio across bases is log_ratio.
This declaration simply records that the identity embedding lies in the class, corresponding to exponent $c=1$.
proof idea
Direct structure instance. The unit field $f(1)=1$ is closed by norm_num. Multiplicativity, after push_cast, is the ring identity $(m\cdot n:\mathbb{R})=(m:\mathbb{R})\cdot(n:\mathbb{R})$. Monotonicity is the integer comparison $m\leq n$ transported by exact_mod_cast. No external lemmas beyond casting and ring arithmetic are used.
why it matters
This is the canonical exponent-one witness inside the MonotoneMultiplicative class that underpins the cost-side power classification. The parent result exists_exponent asserts every nondecreasing completely multiplicative $f$ is a pure power; the identity shows the class is inhabited nontrivially and that $c=1$ is attained. In Recognition Science the cost ledger and the J-cost live on multiplicative structure; a verified identity instance anchors the discrete-to-real passage when reading exponents off cost data. The dependency graph presently records no downstream consumers, so the lemma functions as a local sanity check and a ready hypothesis for applications of the power theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.