Roadmap and non-circularity of the logarithm characterisations

The implication order is one-way until the bridge. The integral function $L$ is defined and proved differentiable, multiplicative-to-additive, unbounded, and bijective without using the published exponential or natural logarithm. Its inverse $E$ is then proved to satisfy $E^{\mathrm{\prime }}=E$ and $E(0)=1$. Only at that point does IVP uniqueness identify $E$ with the published exponential; taking inverses identifies $L$ with the published natural logarithm.

After the bridge, Five characterisations of the natural logarithm are equivalent: inverse exponential, integral, continued Mercator series, Landau root limit and the normalised functional equation compares already proved descriptions: inverse exponential, the integral, the continued Mercator series, the Landau limit, and the regular functional equation. This does not use one description to establish a premise needed earlier in the chain. It is the inverse-function counterpart of the separate exponential roadmap in The power-series, product-limit, IVP, functional-equation, and Picard definitions agree.