MonotoneMultiplicative
plain-language theorem explainer
Packages the three axioms of a completely multiplicative, nondecreasing map from positive integers to reals: value 1 at 1, multiplicativity on arguments at least 1, and monotonicity on that ray. Cost and gauge-orbit work cite it as the exact hypothesis package for Howe's form of Erdős's theorem. As a structure it is pure interface; no proof body.
Claim. A predicate on $f:\mathbb{N}\to\mathbb{R}$ asserting $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$. The value $f(0)$ is left unconstrained.
background
In the cost ledger, characters extracted from rational traces are completely multiplicative on the positive integers and inherit monotonicity from the ledger order (via comparison of traces). The classical target is Erdős's theorem on monotone multiplicative arithmetic functions: under those hypotheses $f$ must be a pure power $n\mapsto n^c$ for a single nonnegative real $c$.
This structure is the Lean packaging of exactly those three conditions, stated only on arguments at least 1 so that the zero slot (which the ledger character does not use) stays free. Upstream native-unit language from the primitive recognition calculus supplies the multiplicative unit $1$, but the structure itself is ordinary real analysis on $\mathbb{N}$.
The module then develops Howe's argument: squeeze powers of $n$ between powers of 2, equate log-ratios, and extract a common exponent.
proof idea
No proof: the declaration is a structure ... : Prop bundling three fields (unit, mul, mono). Inhabitants are built by supplying the three equalities/inequalities, as in the constant-one and identity examples later in the module, or by the extracted nontrivial character in the gauge-orbit classification.
why it matters
This is the hypothesis type for the completely multiplicative case of Erdős's theorem as formalized here (exists_exponent, via log_ratio and the degenerate branch eq_one_of_two_eq_one). Downstream, natChar_monotoneMultiplicative shows that the character pulled from a sans-anchor cost ledger meets precisely these axioms, so the extracted values are a power $n^c$. That power shape is what lets the cost side match the Recognition Composition Law and the forced $J$-cost uniqueness (T5) when characters are read on integer orbits. Without this interface, the Howe/Erdős classification step would have no named target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.