lean_workbook_plus_43566

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Let $s: \mathbb{N} \to \mathbb{N}$ be the successor function, $s(n) = n+1$ . We'll be using the following notation: whenever $f$ and $g$ are functions, $fg$ is the function defined by $fg(x)=f(g(x))$ . Similarly, $f^2=ff$ is just $f(f(x))$ etc. What we know about $f$ can be written as $fs=sf^2$ . So, for all $k \geq 1$ , $fs^k = s^kf^{2^k}$ , which evaluated at $n$ yields $f(n+k) = f^{2^k}(n)+k$ . This holds for $n \geq 1$ and $k \geq 0$ . In particular, setting $n=1$ , $f(k+1) \geq k+1$ . Let $f(1)=x$ and $f(2)=y$ . Then $y=f(x)+1$ . From this it follows that $x \neq 2$ , but if $x \geq 3$ then $f(x) = f(2+x-2) = f^{2^{x-2}}(2)+x-2$ = $f^{2^{x-2}-1}(f(2))+x-2$ so $f^{2^{x-2}-1}(y) = y-x+1$ , which is impossible since $f^m(y) \geq y$ for any $y$ and any $m$ (this follows directly from $f(k) \geq k$ ). So $x$ must be 1, and from $f(1)=1$ it follows immediately by induction that $f(n)=n$ for all $n \in \mathbb{N}$ .

Why this node was retired

The posted statement is

theorem lean_workbook_plus_43566  (f : ℕ → ℕ)
  (h₀ : ∃ x, f x ≠ x)
  (h₁ : ∃ x, f x ≠ x + 1)
  (h₂ : ∀ n, 1 < n → ∀ k, f (n + k) = f^[k] (f n) + k) :
  ∀ n, f n = n   :=  by sorry

On positive integers, assume f(n+1)=f(f(n))+1 and conclude f(n)=n. Remove the invented nonidentity assumptions and replace the erroneous iteration exponent k by the source’s2^k where that derived identity is stated.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

On positive integers, assume f(n+1)=f(f(n))+1 and conclude f(n)=n. Remove the invented nonidentity assumptions and replace the erroneous iteration exponent k by the source’s2^k where that derived identity is stated.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.