pow_eq
plain-language theorem explainer
For a completely multiplicative nondecreasing map f on the positive integers, values on pure powers factor as ordinary powers: f(m^j)=f(m)^j. The squeeze lemmas that pin log-ratios of cost characters cite this identity. Proof is induction on the exponent, using the unit law at 1 and the two-factor multiplicative law.
Claim. Let $f:\mathbb{N}\to\mathbb{R}$ be completely multiplicative and nondecreasing on the positive integers, with $f(1)=1$. Then for every integer $m\ge 1$ and every $j\in\mathbb{N}$, $f(m^j)=f(m)^j$.
background
The ambient structure is a completely multiplicative, nondecreasing real-valued function on the positive integers: $f(1)=1$, $f(mn)=f(m)f(n)$ whenever $m,n\ge 1$, and $m\le n$ (with $m\ge 1$) implies $f(m)\le f(n)$. The value at zero is left free; the cost-ledger character has no content there.
This module develops the elementary power and log-ratio calculus for such maps. Complete multiplicativity on products does not automatically write itself as a power identity in Lean; the present lemma records exactly that extension. Downstream squeeze arguments need $f$ on pure powers $m^j$ and $2^j$ in closed form, nothing more.
proof idea
Term-mode induction on the exponent $j$. The zero case reduces by simpa to the unit law $f(1)=1$. In the successor step one first records $1\le m^j$ from Nat.one_le_pow and the hypothesis $m\ge 1$, then rewrites $m^{j+1}=m^j\cdot m$ and $f(m)^{j+1}=f(m)^j\cdot f(m)$ via pow_succ, applies the two-factor multiplicative law of the structure, and substitutes the inductive hypothesis.
why it matters
The identity is the only power form the squeeze uses. It is applied verbatim in the degenerate branch eq_one_of_two_eq_one: if $f(2)=1$ then $f(2^n)=1$, and monotonicity squeezes every $n$ between 1 and a power of two down to the constant-one character. It is likewise the algebraic engine inside log_ratio, the heart of Howe's argument, which equates $\log(f n)/\log n$ to the base-two ratio by sandwiching $n^k$ between consecutive powers of two and reading the squeeze on both the argument and the value.
In the Recognition cost ledger this pins the admissible characters before the J-cost and forcing chain are imposed: either the map is identically one, or its log-ratio is universal. That dichotomy feeds uniqueness of the cost functional used throughout the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.