IndisputableMonolith.Cost.MonotoneMultiplicativePower
Defines completely multiplicative, nondecreasing maps on the positive integers, with f(0) left free. The structure theorem recovers such maps as pure power laws n ↦ n^α for a unique α ≥ 0. Cost-ledger and gauge-orbit work cite this to pin multiplicative characters of the recognition cost. The argument is classical: multiplicativity plus monotonicity forces the log-ratio to be constant.
claimA map $f:\mathbb{N}\to\mathbb{R}$ is monotone-multiplicative when $f(mn)=f(m)f(n)$ for all $m,n\ge 1$ and $f$ is nondecreasing on $\mathbb{N}_{>0}$. Then $f(n)=n^{\alpha}$ for a unique $\alpha\ge 0$, with $f(0)$ unconstrained.
background
In the Recognition Science cost layer, ledger characters and gauge orbits are constrained by complete multiplicativity on positive integers together with monotonicity. The module isolates that pure arithmetic condition: a function $f$ satisfying $f(mn)=f(m)f(n)$ for $m,n\ge 1$ and $f$ nondecreasing on the positives.
Zero is deliberately excluded from the axioms. The cost ledger's character has no content at $0$, so $f(0)$ may be anything. The only Mathlib import supplies the real-analysis and order infrastructure needed for logarithms and powers.
Sibling lemmas package the elementary consequences: positivity and $f\ge 1$ on $\mathbb{N}_{\ge 1}$, the power identity, the two-equals-one rigidity lemma, the constant log-ratio, and existence of the exponent $\alpha$.
proof idea
The module is a short structure-plus-lemmas package, not a single deep theorem. After the structure MonotoneMultiplicative, one proves $f(1)=1$, positivity, and $f\ge 1$ from multiplicativity and monotonicity. The key step is that $\log f(n)/\log n$ is independent of $n\ge 2$, yielding a unique $\alpha\ge 0$ with $f(n)=n^\alpha$. Constant-one and identity maps are exhibited as the extremal cases $\alpha=0$ and $\alpha=1$.
why it matters in Recognition Science
Gauge-orbit classification in the cost layer imports this module to know that any monotone multiplicative character is a pure power. That pins the admissible scalings of the recognition cost before orbit representatives are chosen. The unit-axiom audit script likewise depends on it when checking that cost normalizations stay inside the forced power family. Within the broader forcing chain, multiplicative cost structure sits upstream of J-uniqueness (T5) and the self-similar fixed point $\phi$ (T6), because the ledger's multiplicative skeleton must already be a power law before the J-functional equation selects the concrete cost.
scope and limits
- Does not constrain f(0); zero is outside the multiplicative domain.
- Does not treat functions on reals or rationals, only natural numbers.
- Does not derive the J-cost or RCL; only the arithmetic skeleton of multiplicative characters.
- Does not force α from physics; α is an arbitrary nonnegative real.
- Does not address decreasing or non-completely-multiplicative maps.