Cost Monotone Multiplicative Power Monotone Multiplicative Const One

The constant function

A completely multiplicative, nondecreasing function on the positive integers is a function f that sends 1 to 1, sends a product m*n to the product f(m)*f(n), and never decreases as its input grows. The constant function that sends every positive integer to 1 satisfies all three conditions. The declaration monotoneMultiplicative_const_one is the machine-checked proof of that fact: it verifies, step by step, that the function f(n) = 1 for all n meets the definition of a completely multiplicative, nondecreasing function.

The proof itself is short. The unit condition holds because 1 = 1. The multiplication condition holds because 1 * 1 = 1. The monotonicity condition holds because 1 ≤ 1. Each line is a direct calculation. The declaration is not a deep theorem; it is a routine verification that a particular simple function belongs to a particular class of functions.

The declaration earns its place because of what surrounds it. In the same file, a theorem proves that every completely multiplicative, nondecreasing function on the positive integers is a power function: there exists a nonnegative real number c such that f(n) = n^c for every n ≥ 1. That theorem has two natural endpoints. The identity function f(n) = n realizes the exponent c = 1. The constant function f(n) = 1 realizes the exponent c = 0. The declaration monotoneMultiplicative_const_one supplies the second endpoint, showing that the theorem's conclusion is not vacuous: the class of functions it describes actually contains the constant function.

The declaration does not claim that the constant function is the only completely multiplicative, nondecreasing function. It does not claim that the constant function arises from any particular cost structure. It does not claim that the exponent c = 0 is forced by the conditions. It only establishes that the constant function is one member of the class. The theorem that every member of the class is a power function is a separate statement, proved elsewhere in the file.

In the broader framework of Recognition Science, this lemma plays a supporting role. The framework models cost as a function on a discrete ledger of events, and it proves that any cost function satisfying certain conditions must equal J(x) = (x + 1/x)/2 - 1. The classification of completely multiplicative, nondecreasing functions is a tool used in that derivation. The constant function is the degenerate case, the exponent-zero endpoint of the classification. The declaration pins down that endpoint cleanly, so that the classification theorem can state its full range of possibilities without leaving a gap.

theorem monotoneMultiplicative_const_one : MonotoneMultiplicative (fun _ : ℕ => (1 : ℝ)) where
  unit := rfl
  mul := by intro m n _ _; norm_num
  mono := by intro m n _ _; exact le_rfl

What this page does not claim

The constant function is the only completely multiplicative, nondecreasing function. The constant function is forced by the conditions of the classification theorem. The constant function corresponds to any particular physical cost structure.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/MonotoneMultiplicativePower.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: