monotoneMultiplicative_const_one
plain-language theorem explainer
The constant map n ↦ 1 on the naturals is completely multiplicative and nondecreasing on the positive integers. It is the exponent-zero endpoint of the completely multiplicative case of Erdős's theorem (Howe's proof). The proof is a three-field structure instance: unit by reflexivity, multiplicativity by norm_num, monotonicity by reflexivity of ≤.
Claim. The constant function $f:\mathbb{N}\to\mathbb{R}$ given by $f(n)=1$ satisfies $f(1)=1$, $f(mn)=f(m)f(n)$ whenever $m,n\ge 1$, and $f(m)\le f(n)$ whenever $1\le m\le n$.
background
The ambient structure packages a completely multiplicative, nondecreasing real-valued function on the positive integers: $f(1)=1$, $f(mn)=f(m)f(n)$ for $m,n\ge 1$, and $m\le n$ (with $m\ge 1$) implies $f(m)\le f(n)$. The value at $0$ is left unconstrained, matching the cost-ledger character which has no content there.
The module proves Erdős's theorem in the completely multiplicative case (Howe's argument): every such $f$ is a power $n\mapsto n^c$ for a single nonnegative real exponent $c$. The nonvacuity section records that the hypothesis class is inhabited at both ends of the conclusion: the constant function realizes exponent zero and the identity realizes exponent one.
proof idea
Direct structure instance for the constant function $n\mapsto 1$. The unit field is rfl ($1=1$). Multiplicativity is discharged by norm_num on $1\cdot 1=1$. Monotonicity is le_rfl (equality is a special case of $\le$). No external lemmas beyond the structure definition are required.
why it matters
Supplies the exponent-zero witness in the nonvacuity pack for the completely multiplicative Erdős theorem (exists_exponent). Without an inhabited hypothesis class the power classification would be vacuous. The companion identity instance supplies exponent one; together they show monotonicity is doing real work (the Liouville function is completely multiplicative yet not a power). In the Recognition cost layer this anchors the degenerate flat character before nontrivial monotone multiplicative costs are classified as pure powers on the naturals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.