Power law characterisation of the generic logarithm

As in the last posting, we begin by asserting the existence of a function from the positive reals onto a set `L`,

`\qquad\qquad\qquad "lg":RR^+ \rightarrow L`.

Also, as stated in the last posting, "the log of a product is the sum of the logs of the factors" is not the only way to characterise the generic logarithm.

We can instead simply assert the end result of the last posting, and let that be our entire starting condition.

That is, for all positive real `x` and all real `p`, we assert that

`\qquad\qquad\qquad "lg"(x^p) = p\cdot"lg"(x).`

This defines multiplication of quantities in `L` by arbitrary real numbers.  Let us call this, with some degree of anticipation, the "scalar multiplication" condition.  As before, the existence of models ensures the consistency of the definition.

Consider now arbitrary positive real numbers `u` and `v`.  Then for arbitrary positive real `x \ne 1`, we can find `p` and `q` such that `u = x^p` and `v = x^q`.  Then

`\qquad\qquad\qquad "lg"(u v) = "lg"(x^p x^q)`,
`\qquad\qquad\qquad\qquad = "lg"(x^{p+q})`,
`\qquad\qquad\qquad\qquad = (p+q)\cdot"lg"(x)`,
`\qquad\qquad\qquad\qquad = p\cdot"lg"(x) + q\cdot"lg"(x)`,
`\qquad\qquad\qquad\qquad = "lg"(x^p) + "lg"(x^q)`,
`\qquad\qquad\qquad\qquad = "lg"(u) + "lg"(v)`.

and we have established the "the log of a product is the sum of the logs of the factors" condition with which we began the last posting. 

From this we could derive all subsequent results just as we did there---but that would be wasteful, as most of those results are simply instances of the scalar multiplication condition.

We can also use the scalar multiplication condition to define division in `L`, at least for `x \ne 1` (with the consequence that `"lg"(x) \ne 0)`.  In that case, we have

`\qquad\qquad\qquad \frac{"lg"(x^p)}{"lg"(x)} = p.`

Since, given any positive real `x` and `y`, we can find a unique real number `p` such that `y = x^p`, we can divide any quantity in `L` by any nonzero quantity in `L`.