Cost Monotone Multiplicative Power One Le

The lower bound

A cost function in this framework assigns a real number to each positive integer, a number meant to represent the cost of recognizing that integer as a distinct object. The declaration one_le establishes a simple lower bound: if the function is completely multiplicative (the cost of a product is the product of the costs) and nondecreasing (larger arguments never cost less), and if the cost of 1 is exactly 1, then the cost of every positive integer is at least 1. The proof is immediate: since 1 ≤ n, monotonicity gives f(1) ≤ f(n), and the unit condition f(1) = 1 closes the inequality.

This bound is the first rung of a larger result. The same three conditions, complete multiplicativity, monotonicity, and the unit value, force the entire function to be a pure power: there exists a nonnegative real exponent c such that f(n) = n^c for every positive n. The lower bound one_le is what rules out exponents below zero, so that the constant function (exponent 0) and the identity function (exponent 1) both satisfy the conditions, and no function that dips below 1 can enter the class. The proof of the power form is due to Erdős, in the completely multiplicative case, and the machine-checked version here follows a squeeze argument attributed to Howe: it pins n^k between powers of 2, reads the monotonicity squeeze twice, and lets k grow.

What one_le does not claim is just as important as what it proves. It does not assert that the cost of every integer is strictly greater than 1; the constant function f(n) = 1 is a legitimate member of the class, so equality is allowed. It also does not apply to the value at 0: the conditions are stated only for positive arguments, and the value f(0) is left unconstrained, since the ledger has no content there. And the theorem does not by itself identify the exponent c; it only guarantees that a nonnegative exponent exists. The uniqueness of that exponent, and its connection to the golden ratio, belongs to later steps in the forcing chain.

In the broader Recognition Science account, this bound is what keeps the cost ledger honest: no positive integer can be recognized at a cost below the cost of recognizing 1. That single constraint, together with multiplicativity and monotonicity, is enough to reduce the entire space of candidate cost functions to a one-parameter family of powers, a family whose members are all nonnegative and well-behaved. The theorem is a small but load-bearing piece of the framework's foundation, and its proof is checked by a machine.

theorem one_le (hf : MonotoneMultiplicative f) {n : ℕ} (hn : 1 ≤ n) : 1 ≤ f n := by
  have h := hf.mono 1 n le_rfl hn
  rwa [hf.unit] at h

/-- **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 monotoneMultiplicative_const_one : MonotoneMultiplicative (fun _ : ℕ => (1 : ℝ)) where
  unit := rfl
  mul := by intro m n _ _; norm_num
  mono := by intro m n _ _; exact le_rfl

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

The theorem does not assert that the cost of every integer is strictly greater than 1; the constant function f(n) = 1 is allowed. The theorem does not apply to the value at 0, which is left unconstrained. The theorem does not identify the specific exponent c; it only guarantees that a nonnegative exponent exists.

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: