one_le

The structure packing the hypotheses requires three axioms on $f:\mathbb{N}\to\mathbb{R}$: the unit law $f(1)=1$, complete multiplicativity $f(mn)=f(m)f(n)$ whenever $m,n\ge 1$, and monotonicity ($1\le m\le n$ implies $f(m)\le f(n)$). The value $f(0)$ is deliberately unconstrained; the cost-ledger character has no content at zero.

The local setting is the Cost module's study of integer-scaling behaviour of recognition cost. The same package is the standing hypothesis for Howe's proof that every such $f$ is a pure power $n\mapsto n^c$ with a single nonnegative real exponent (the completely multiplicative case of Erdős's theorem).

Monotonicity applied to the pair $1\le n$ yields $f(1)\le f(n)$. The unit axiom rewrites the left-hand side as $1$, giving the claim. Term proof: one have from the mono field, then rwa with the unit field.

Direct input to three siblings. Positivity is the strict bound $0<f(n)$ obtained by chaining $0<1\le f(n)$. The degenerate-branch lemma uses the lower bound to squeeze every value to 1 once $f(2)=1$ (every $n$ sits below a power of two). The main classification theorem case-splits on $f(2)=1$ versus $f(2)>1$; the lower bound supplies both the constant-function branch (exponent zero) and nonnegativity of the candidate exponent in the nondegenerate branch.

In Recognition Science the cost ledger produces characters of exactly this shape. Identifying them as pure powers $n^c$ is the bridge from discrete recognition counts to continuous scaling on the phi-ladder.