lean_workbook_plus_13566

⚠️ 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.

I'll assume that $f(b) = 1$ and $a\ne b$ . \n\nLet $x = y = 1$ ; we get that $f(1)^2 + 1 = 2f(1)\Rightarrow f(1) = 1$ . Then let $y = 1$ to get $f(x) = f\left(\frac {a}{x}\right)$ for all positive reals $x$ ; letting $x = 1$ gives a similar expression for $b$ ; we hence have that $f(t) = f(a/t) = f(b/t)$ for any positive real $t$ ; then $f(t) = f(a^mb^nt)$ for any integers $m,n$ by recursively using this. If $f$ is continuous, this solves the problem, but I'm not sure if the conclusion is true if the function doesn't have to be continuous.

Why this node was retired

The posted statement is

theorem lean_workbook_plus_13566  (a b : ℝ)
  (f : ℝ → ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ a ≠ b)
  (h₁ : Continuous f)
  (h₂ : ∀ x, 0 < x → f (a * x) = f (x) + f (a / x))
  (h₃ : ∀ x, 0 < x → f (b * x) = f (x) + f (b / x)) :
  ∀ x, 0 < x → f x = 1   :=  by sorry

The excerpt refers to f(b)=1 and prior hypotheses that are not represented, so an exact replacement classification is unavailable.

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

Proposed corrected statement

Recover the original functional equation and normalization from the full source before specifying the function; remove the added incompatible global-scaling model and its invented constant answer.

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.