exists_exponent
plain-language theorem explainer
A nondecreasing completely multiplicative map f : ℕ → ℝ is a pure power: there is a single c ≥ 0 with f(n) = n^c for all n ≥ 1. The constant-one map is the c = 0 case. Anyone classifying cost characters or gauge orbits cites this (Howe's form of Erdős). The proof splits on f(2) = 1 versus f(2) > 1, then applies the log-ratio squeeze at base two.
Claim. Let $f : \mathbb{N} \to \mathbb{R}$ satisfy $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)$. Then there exists $c \ge 0$ such that $f(n) = n^c$ for every integer $n \ge 1$.
background
The ambient structure is a completely multiplicative nondecreasing real function on the positive integers: $f(1)=1$, $f(mn)=f(m)f(n)$ for $m,n\ge 1$, and $f$ nondecreasing on that range. The value at zero is left free; cost characters carry no content there.
The classical statement is Erdős's theorem on monotone multiplicative arithmetic functions, specialized to the completely multiplicative case and proved in Howe's form. Two local lemmas prepare the ground. If $f(2)=1$, then $f$ is identically one on $\mathbb{N}_{\ge 1}$, by sandwiching each $n$ below a power of two and using multiplicativity plus monotonicity. If $f(2)>1$, the heart of the argument is the log-ratio identity: $\log(f n)\cdot\log 2 = \log(f 2)\cdot\log n$ for every $n\ge 2$, obtained by squeezing powers of $n$ between consecutive powers of two and reading the squeeze on both the argument and the value.
The module also records nonvacuity: the constant function realizes exponent zero and the identity realizes exponent one, so the hypothesis class is inhabited at both ends of the conclusion.
proof idea
From monotonicity one has $f(2)\ge f(1)=1$. Split on equality versus strict inequality.
If $f(2)=1$, take $c=0$. The zero-power identity $n^0=1$ together with the degenerate-branch lemma (every $n\ge 1$ satisfies $f(n)=1$) finishes the claim.
If $f(2)>1$, set $c=\log(f 2)/\log 2$, which is positive. For $n=1$ use the unit axiom and $1^c=1$. For $n\ge 2$ invoke the log-ratio lemma, rewrite $n^c$ via $\mathrm{rpow_def}$ and $\exp\circ\log$, and clear the resulting linear relation by field simplification and linarith.
why it matters
This is the real-exponent step in the cost-character classification. Downstream, exists_nat_exponent in GaugeOrbitClassification quotes it directly: Howe supplies the real $c$, the anchor root forces positivity, and the six-exponentials input upgrades $c$ to a positive integer. That integer exponent is what lets gauge orbits be read as pure powers rather than arbitrary multiplicative characters.
In the Recognition ledger this pins the shape of native cost on ratio orbits: once a character is monotone and completely multiplicative, it cannot wander; it is $n\mapsto n^c$. The degenerate $c=0$ branch is identified separately as the pure orientation (sign) gauge, which charges reversal and ignores magnitude. The result therefore separates magnitude-sensitive cost from orientation-only cost, a distinction used when ruling out non-canonical cube-generated ledgers and when auditing that cost-unit hypotheses enter as named assumptions rather than ambient axioms.
Relative to the forcing chain, this sits on the cost-algebra side that feeds J-automorphisms and the uniqueness story for the J-cost, rather than on T5–T8 themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.