lean_workbook_plus_56536

⚠️ 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 $g(x) = f(x) - x$. Then, by the original equation, $g(x) \ge 0$ and $g(g(x)) = 2x - g(x)$. Fix $x$ and let $a_n = g^n(x)$ be the $n$-th iterate of $g$. Then, $a_{n+2} = 2a_n - a_{n+1}$, and solving the recurrence we get that $a_n = \frac{2x+g(x)}{3} + \frac{x-g(x)}{3}(-2)^n$, Contradicting $g(x) \ge 0$ for some large $n$, unless $g(x) = x$. Therefore, $f(x) = 2x$, which is a solution.

Why this node was retired

The posted statement is

theorem lean_workbook_plus_56536  (f : ℝ → ℝ)
  (h₀ : ∃ x, 0 ≤ f x)
  (h₁ : ∃ x, 0 ≤ f (f x))
  (h₂ : ∀ x, f (f x) = 2 * x - f x) :
  ∀ x, f x = 2 * x   :=  by sorry

The transformed function g is confused with f, universal nonnegativity is weakened to two existential facts, and the conclusion for f is asserted for g.

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

Proposed corrected statement

State g(x)=f(x)−x on the original domain, restore the exact universal nonnegativity and iterate equation for g, derive g(x)=x, then conclude f(x)=2x. Recover the domain since g≥0 on all ℝ is incompatible with g=id.

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.