Must a finite-subset choice function on a set of size $\aleph_\omega$ admit an infinite independent set? (Erdős #623)

Let $X$ be a set of cardinality $\aleph_\omega$ and let $f$ be a function from the finite subsets of $X$ to $X$ satisfying $f(A)\notin A$ for every finite $A\subseteq X$. Call a subset $Y\subseteq X$ independent for $f$ if for every finite $B\subset Y$ we have $f(B)\notin Y$. Must there always exist an infinite independent set $Y\subseteq X$? This is a set-mapping (free-set) problem: $f$ assigns to each finite configuration a point avoiding it, and one seeks an infinite subset closed under 'no chosen point falls back inside'.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, else fully written) that for every $f$ from the finite subsets of a set $X$ of cardinality $\aleph_\omega$ into $X$ with $f(A)\notin A$ there is an infinite independent $Y$; OR an explicit $f$ (with a verification that it has no infinite independent set) showing the answer is no; OR a proof that the statement is independent of ZFC, i.e. models of ZFC realising each answer (e.g. a forcing extension with a counterexample together with a model where every such $f$ has an infinite independent set). ADVANCES (each fully proved): settle the analogous question at a specific singular or successor cardinal above $\aleph_\omega$; establish a positive answer under a stated hypothesis (e.g. a large-cardinal or PCF assumption) or a negative answer under another; formalise the Erdős–Hajnal $\lvert X\rvert<\aleph_\omega$ construction and the $\aleph_\omega$ statement in Lean; or bound the least size of $Y$ obtainable. Deliver the proof/formalisation, or the explicit $f$ with its no-independent-set certificate.