Encyclopedia Cost Cost Monotone Multiplicative Power
ARTICLE 4 claims 4 theorems
Cost Monotone Multiplicative Power
A simple rule about how costs scale forces them to follow a single power law, and the proof is a squeeze between powers of two.
The power law
A completely multiplicative, nondecreasing function on the positive integers is a function f where f(1) = 1, f(m*n) = f(m)*f(n) for all positive m and n, and f(m) ≤ f(n) whenever m ≤ n. The classical theorem, due to Erdős, says that any such function must be a power: there is a single nonnegative real exponent c such that f(n) = n^c for every positive integer n. The constant function 1 is the case c = 0, and the identity function is the case c = 1.
The proof, due to Howe, is a squeeze. For any base n ≥ 2, compare n^k with powers of two. Since n^k lies between 2^j and 2^(j+1) for some j, monotonicity gives f(2)^j ≤ f(n)^k ≤ f(2)^(j+1). Letting k grow forces the ratio log(f(n))/log(n) to equal log(f(2))/log(2), so the exponent is the same for every base. The degenerate case f(2) = 1 collapses everything to the constant function, because every integer is below some power of two.
In Recognition Science, the cost ledger is a discrete record of recognition events, and the cost of recognition is forced, not chosen. This result applies the classical theorem to show that any cost function satisfying the monotone multiplicative conditions must be a power function. The framework's library of machine-checked formal theorems proves the existence of the exponent c and verifies that both the constant and identity functions are valid instances.
The result matters because it constrains what a cost function can look like: no exotic, non-power behavior is possible under these plain conditions. Monotonicity is essential; without it, the Liouville function, which is completely multiplicative but not a power, would be a counterexample. The theorem is not vacuous, as the constant and identity functions inhabit the hypothesis class.
THEOREM exists_exponent · IndisputableMonolith/Cost/MonotoneMultiplicativePower.lean
/-- **Erdős's theorem, completely multiplicative case (Howe's proof).** A nondecreasing
completely multiplicative function on the positive integers is a power, with a single
nonnegative real exponent. The degenerate constant function is the exponent zero. -/
theorem exists_exponent (hf : MonotoneMultiplicative f) :
∃ c : ℝ, 0 ≤ c ∧ ∀ n : ℕ, 1 ≤ n → f n = (n : ℝ) ^ c := by
rcases eq_or_lt_of_le (one_le hf (by norm_num : (1 : ℕ) ≤ 2)) with h2 | h2
· refine ⟨0, le_rfl, fun n hn => ?_⟩
rw [Real.rpow_zero, eq_one_of_two_eq_one hf h2.symm hn]
· have hL2 : 0 < Real.log 2 := Real.log_pos (by norm_num)
have hM2 : 0 < Real.log (f 2) := Real.log_pos h2
refine ⟨Real.log (f 2) / Real.log 2, le_of_lt (div_pos hM2 hL2), fun n hn => ?_⟩
rcases eq_or_lt_of_le hn with h1 | h1
· have hn1 : n = 1 := h1.symm
subst hn1
rw [hf.unit, Nat.cast_one, Real.one_rpow]
· have hn2 : 2 ≤ n := h1
have hlog := log_ratio hf h2 hn2
have hnpos : (0 : ℝ) < (n : ℝ) := by
exact_mod_cast lt_of_lt_of_le Nat.zero_lt_one hn
have hfpos : 0 < f n := pos hf hn
rw [Real.rpow_def_of_pos hnpos, ← Real.exp_log hfpos]
congr 1
field_simp
linarith [hlog]
THEOREM log_ratio · IndisputableMonolith/Cost/MonotoneMultiplicativePower.lean
/-- **The heart of Howe's argument.** For every base `n ≥ 2` the ratio
`log (f n) / log n` is the same as at the base two, stated cross-multiplied so that no
division appears. The proof squeezes `n ^ k` between `2 ^ j` and `2 ^ (j+1)`, reads the
squeeze twice (on the argument and on the value), and lets `k` grow. -/
theorem log_ratio (hf : MonotoneMultiplicative f) (h2 : 1 < f 2) {n : ℕ} (hn : 2 ≤ n) :
Real.log (f n) * Real.log 2 = Real.log (f 2) * Real.log n := by
set L2 := Real.log 2 with hL2def
set Ln := Real.log n with hLndef
set M2 := Real.log (f 2) with hM2def
set Mn := Real.log (f n) with hMndef
have hnR : (1 : ℝ) < (n : ℝ) := by exact_mod_cast lt_of_lt_of_le one_lt_two hn
have hL2 : 0 < L2 := Real.log_pos (by norm_num)
have hLn : 0 < Ln := Real.log_pos hnR
have hM2 : 0 < M2 := Real.log_pos h2
have hfn : 1 < f n := lt_of_lt_of_le h2 (hf.mono 2 n (by norm_num) hn)
have hMn : 0 < Mn := Real.log_pos hfn
have hn1 : 1 ≤ n := le_trans (by norm_num) hn
have key : ∀ k : ℕ, 1 ≤ k → (k : ℝ) * |Mn * L2 - M2 * Ln| ≤ M2 * L2 := by
intro k hk
set j := Nat.log 2 (n ^ k) with hjdef
have hnkpos : 1 ≤ n ^ k := Nat.one_le_pow k n (by omega)
have hnk0 : n ^ k ≠ 0 := by omega
have hle : 2 ^ j ≤ n ^ k := Nat.pow_log_le_self 2 hnk0
have hlt : n ^ k < 2 ^ (j + 1) := Nat.lt_pow_succ_log_self (by norm_num) _
have hleR : ((2 : ℝ)) ^ j ≤ ((n : ℝ)) ^ k := by exact_mod_cast hle
have hltR : ((n : ℝ)) ^ k ≤ ((2 : ℝ)) ^ (j + 1) := by exact_mod_cast hlt.le
have ha : (j : ℝ) * L2 ≤ (k : ℝ) * Ln := by
have h := Real.log_le_log (by positivity) hleR
rwa [Real.log_pow, Real.log_pow] at h
have hb : (k : ℝ) * Ln ≤ ((j : ℝ) + 1) * L2 := by
have h := Real.log_le_log (by positivity) hltR
rw [Real.log_pow, Real.log_pow] at h
push_cast at h
linarith
have hf2j : 1 ≤ 2 ^ j := Nat.one_le_pow j 2 (by norm_num)
have hf2j1 : 1 ≤ 2 ^ (j + 1) := Nat.one_le_pow (j + 1) 2 (by norm_num)
have hfa : f (2 ^ j) ≤ f (n ^ k) := hf.mono _ _ hf2j hle
have hfb : f (n ^ k) ≤ f (2 ^ (j + 1)) := hf.mono _ _ (Nat.one_le_pow k n (by omega)) hlt.le
rw [pow_eq hf (by norm_num) j, pow_eq hf hn1 k] at hfa
rw [pow_eq hf hn1 k, pow_eq hf (by norm_num) (j + 1)] at hfb
have hf2pos : (0 : ℝ) < f 2 := lt_trans zero_lt_one h2
have hfnpos : (0 : ℝ) < f n := lt_trans zero_lt_one hfn
have hc : (j : ℝ) * M2 ≤ (k : ℝ) * Mn := by
have h := Real.log_le_log (by positivity) hfa
rwa [Real.log_pow, Real.log_pow] at h
have hd : (k : ℝ) * Mn ≤ ((j : ℝ) + 1) * M2 := by
have h := Real.log_le_log (by positivity) hfb
rw [Real.log_pow, Real.log_pow] at h
push_cast at h
linarith
have e1 : ((k : ℝ) * Mn) * L2 ≤ (((j : ℝ) + 1) * M2) * L2 :=
mul_le_mul_of_nonneg_right hd hL2.le
have e2 : ((j : ℝ) * L2) * M2 ≤ ((k : ℝ) * Ln) * M2 :=
mul_le_mul_of_nonneg_right ha hM2.le
have e3 : ((j : ℝ) * M2) * L2 ≤ ((k : ℝ) * Mn) * L2 :=
mul_le_mul_of_nonneg_right hc hL2.le
have e4 : ((k : ℝ) * Ln) * M2 ≤ (((j : ℝ) + 1) * L2) * M2 :=
mul_le_mul_of_nonneg_right hb hM2.le
have habs : |(k : ℝ) * (Mn * L2 - M2 * Ln)| ≤ M2 * L2 := by
rw [abs_le]
constructor
· nlinarith [e3, e4]
· nlinarith [e1, e2]
calc (k : ℝ) * |Mn * L2 - M2 * Ln|
= |(k : ℝ) * (Mn * L2 - M2 * Ln)| := by
rw [abs_mul, Nat.abs_cast]
_ ≤ M2 * L2 := habs
by_contra hne
have hD : 0 < |Mn * L2 - M2 * Ln| := abs_pos.mpr (sub_ne_zero_of_ne hne)
obtain ⟨k, hk⟩ := exists_nat_gt ((M2 * L2) / |Mn * L2 - M2 * Ln|)
have hbig : M2 * L2 < (k : ℝ) * |Mn * L2 - M2 * Ln| := (div_lt_iff₀ hD).mp hk
have hsmall := key (k + 1) (Nat.le_add_left 1 k)
push_cast at hsmall
nlinarith [hD, hbig, hsmall]
THEOREM eq_one_of_two_eq_one · IndisputableMonolith/Cost/MonotoneMultiplicativePower.lean
/-- The degenerate branch. If the value at two is one then every value is one, because
every integer is below a power of two and the values in between are squeezed. -/
theorem eq_one_of_two_eq_one (hf : MonotoneMultiplicative f) (h2 : f 2 = 1)
{n : ℕ} (hn : 1 ≤ n) : f n = 1 := by
have hlt : n < 2 ^ n := Nat.lt_two_pow_self
have hle := hf.mono n (2 ^ n) hn hlt.le
rw [pow_eq hf (by norm_num) n, h2, one_pow] at hle
exact le_antisymm hle (one_le hf hn)
THEOREM monotoneMultiplicative_id · IndisputableMonolith/Cost/MonotoneMultiplicativePower.lean
theorem monotoneMultiplicative_id : MonotoneMultiplicative (fun n : ℕ => (n : ℝ)) where
unit := by norm_num
mul := by intro m n _ _; push_cast; ring
mono := by intro m n _ hmn; exact_mod_cast hmn
What this page does not claim
This does not claim that the exponent c is the golden ratio or any specific number. This does not claim that the result applies to functions defined at zero. This does not claim that the Liouville function satisfies the monotonicity condition.
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:
- What does the exponent c represent physically in the cost ledger?
- How does this power law connect to the golden ratio forcing chain?
- What other classical theorems about multiplicative functions have analogues in the framework?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM exists_exponent · IndisputableMonolith/Cost/MonotoneMultiplicativePower.lean
/-- **Erdős's theorem, completely multiplicative case (Howe's proof).** A nondecreasing completely multiplicative function on the positive integers is a power, with a single nonnegative real exponent. The degenerate constant function is the exponent zero. -/ theorem exists_exponent (hf : MonotoneMultiplicative f) : ∃ c : ℝ, 0 ≤ c ∧ ∀ n : ℕ, 1 ≤ n → f n = (n : ℝ) ^ c := by rcases eq_or_lt_of_le (one_le hf (by norm_num : (1 : ℕ) ≤ 2)) with h2 | h2 · refine ⟨0, le_rfl, fun n hn => ?_⟩ rw [Real.rpow_zero, eq_one_of_two_eq_one hf h2.symm hn] · have hL2 : 0 < Real.log 2 := Real.log_pos (by norm_num) have hM2 : 0 < Real.log (f 2) := Real.log_pos h2 refine ⟨Real.log (f 2) / Real.log 2, le_of_lt (div_pos hM2 hL2), fun n hn => ?_⟩ rcases eq_or_lt_of_le hn with h1 | h1 · have hn1 : n = 1 := h1.symm subst hn1 rw [hf.unit, Nat.cast_one, Real.one_rpow] · have hn2 : 2 ≤ n := h1 have hlog := log_ratio hf h2 hn2 have hnpos : (0 : ℝ) < (n : ℝ) := by exact_mod_cast lt_of_lt_of_le Nat.zero_lt_one hn have hfpos : 0 < f n := pos hf hn rw [Real.rpow_def_of_pos hnpos, ← Real.exp_log hfpos] congr 1 field_simp linarith [hlog]A completely multiplicative, nondecreasing function on the positive integers must be a power: there is a single nonnegative real exponent c such that f(n) = n^c for every positive integer n. exists_exponent · IndisputableMonolith/Cost/MonotoneMultiplicativePower.leanTHEOREM log_ratio · IndisputableMonolith/Cost/MonotoneMultiplicativePower.lean
/-- **The heart of Howe's argument.** For every base `n ≥ 2` the ratio `log (f n) / log n` is the same as at the base two, stated cross-multiplied so that no division appears. The proof squeezes `n ^ k` between `2 ^ j` and `2 ^ (j+1)`, reads the squeeze twice (on the argument and on the value), and lets `k` grow. -/ theorem log_ratio (hf : MonotoneMultiplicative f) (h2 : 1 < f 2) {n : ℕ} (hn : 2 ≤ n) : Real.log (f n) * Real.log 2 = Real.log (f 2) * Real.log n := by set L2 := Real.log 2 with hL2def set Ln := Real.log n with hLndef set M2 := Real.log (f 2) with hM2def set Mn := Real.log (f n) with hMndef have hnR : (1 : ℝ) < (n : ℝ) := by exact_mod_cast lt_of_lt_of_le one_lt_two hn have hL2 : 0 < L2 := Real.log_pos (by norm_num) have hLn : 0 < Ln := Real.log_pos hnR have hM2 : 0 < M2 := Real.log_pos h2 have hfn : 1 < f n := lt_of_lt_of_le h2 (hf.mono 2 n (by norm_num) hn) have hMn : 0 < Mn := Real.log_pos hfn have hn1 : 1 ≤ n := le_trans (by norm_num) hn have key : ∀ k : ℕ, 1 ≤ k → (k : ℝ) * |Mn * L2 - M2 * Ln| ≤ M2 * L2 := by intro k hk set j := Nat.log 2 (n ^ k) with hjdef have hnkpos : 1 ≤ n ^ k := Nat.one_le_pow k n (by omega) have hnk0 : n ^ k ≠ 0 := by omega have hle : 2 ^ j ≤ n ^ k := Nat.pow_log_le_self 2 hnk0 have hlt : n ^ k < 2 ^ (j + 1) := Nat.lt_pow_succ_log_self (by norm_num) _ have hleR : ((2 : ℝ)) ^ j ≤ ((n : ℝ)) ^ k := by exact_mod_cast hle have hltR : ((n : ℝ)) ^ k ≤ ((2 : ℝ)) ^ (j + 1) := by exact_mod_cast hlt.le have ha : (j : ℝ) * L2 ≤ (k : ℝ) * Ln := by have h := Real.log_le_log (by positivity) hleR rwa [Real.log_pow, Real.log_pow] at h have hb : (k : ℝ) * Ln ≤ ((j : ℝ) + 1) * L2 := by have h := Real.log_le_log (by positivity) hltR rw [Real.log_pow, Real.log_pow] at h push_cast at h linarith have hf2j : 1 ≤ 2 ^ j := Nat.one_le_pow j 2 (by norm_num) have hf2j1 : 1 ≤ 2 ^ (j + 1) := Nat.one_le_pow (j + 1) 2 (by norm_num) have hfa : f (2 ^ j) ≤ f (n ^ k) := hf.mono _ _ hf2j hle have hfb : f (n ^ k) ≤ f (2 ^ (j + 1)) := hf.mono _ _ (Nat.one_le_pow k n (by omega)) hlt.le rw [pow_eq hf (by norm_num) j, pow_eq hf hn1 k] at hfa rw [pow_eq hf hn1 k, pow_eq hf (by norm_num) (j + 1)] at hfb have hf2pos : (0 : ℝ) < f 2 := lt_trans zero_lt_one h2 have hfnpos : (0 : ℝ) < f n := lt_trans zero_lt_one hfn have hc : (j : ℝ) * M2 ≤ (k : ℝ) * Mn := by have h := Real.log_le_log (by positivity) hfa rwa [Real.log_pow, Real.log_pow] at h have hd : (k : ℝ) * Mn ≤ ((j : ℝ) + 1) * M2 := by have h := Real.log_le_log (by positivity) hfb rw [Real.log_pow, Real.log_pow] at h push_cast at h linarith have e1 : ((k : ℝ) * Mn) * L2 ≤ (((j : ℝ) + 1) * M2) * L2 := mul_le_mul_of_nonneg_right hd hL2.le have e2 : ((j : ℝ) * L2) * M2 ≤ ((k : ℝ) * Ln) * M2 := mul_le_mul_of_nonneg_right ha hM2.le have e3 : ((j : ℝ) * M2) * L2 ≤ ((k : ℝ) * Mn) * L2 := mul_le_mul_of_nonneg_right hc hL2.le have e4 : ((k : ℝ) * Ln) * M2 ≤ (((j : ℝ) + 1) * L2) * M2 := mul_le_mul_of_nonneg_right hb hM2.le have habs : |(k : ℝ) * (Mn * L2 - M2 * Ln)| ≤ M2 * L2 := by rw [abs_le] constructor · nlinarith [e3, e4] · nlinarith [e1, e2] calc (k : ℝ) * |Mn * L2 - M2 * Ln| = |(k : ℝ) * (Mn * L2 - M2 * Ln)| := by rw [abs_mul, Nat.abs_cast] _ ≤ M2 * L2 := habs by_contra hne have hD : 0 < |Mn * L2 - M2 * Ln| := abs_pos.mpr (sub_ne_zero_of_ne hne) obtain ⟨k, hk⟩ := exists_nat_gt ((M2 * L2) / |Mn * L2 - M2 * Ln|) have hbig : M2 * L2 < (k : ℝ) * |Mn * L2 - M2 * Ln| := (div_lt_iff₀ hD).mp hk have hsmall := key (k + 1) (Nat.le_add_left 1 k) push_cast at hsmall nlinarith [hD, hbig, hsmall]The proof squeezes n^k between powers of two and lets k grow to force the exponent to be the same for every base. log_ratio · IndisputableMonolith/Cost/MonotoneMultiplicativePower.leanTHEOREM eq_one_of_two_eq_one · IndisputableMonolith/Cost/MonotoneMultiplicativePower.lean
/-- The degenerate branch. If the value at two is one then every value is one, because every integer is below a power of two and the values in between are squeezed. -/ theorem eq_one_of_two_eq_one (hf : MonotoneMultiplicative f) (h2 : f 2 = 1) {n : ℕ} (hn : 1 ≤ n) : f n = 1 := by have hlt : n < 2 ^ n := Nat.lt_two_pow_self have hle := hf.mono n (2 ^ n) hn hlt.le rw [pow_eq hf (by norm_num) n, h2, one_pow] at hle exact le_antisymm hle (one_le hf hn)If f(2) = 1, then f is the constant function 1. eq_one_of_two_eq_one · IndisputableMonolith/Cost/MonotoneMultiplicativePower.leanTHEOREM monotoneMultiplicative_id · IndisputableMonolith/Cost/MonotoneMultiplicativePower.lean
theorem monotoneMultiplicative_id : MonotoneMultiplicative (fun n : ℕ => (n : ℝ)) where unit := by norm_num mul := by intro m n _ _; push_cast; ring mono := by intro m n _ hmn; exact_mod_cast hmnMonotonicity cannot be dropped: the Liouville function is completely multiplicative and is no power. monotoneMultiplicative_id · IndisputableMonolith/Cost/MonotoneMultiplicativePower.lean