GCH set mappings on $\aleph_{\omega+1}$ with small intersections: is there a full-size free set? (Erdős #1173)

Assume the generalised continuum hypothesis (GCH). Let$$f: \omega_{\omega+1}\to [\omega_{\omega+1}]^{\leq \aleph_\omega}$$be a set mapping (so each $f(\alpha)$ is a subset of $\omega_{\omega+1}$ of cardinality at most $\aleph_\omega$) such that$$\lvert f(\alpha)\cap f(\beta)\rvert <\aleph_\omega$$for all $\alpha\neq \beta$. Must there exist a free set of cardinality $\aleph_{\omega+1}$ — a set $X\subseteq \omega_{\omega+1}$ with $\lvert X\rvert = \aleph_{\omega+1}$ such that $\alpha\notin f(\beta)$ for all distinct $\alpha,\beta\in X$?

Acceptance. FULLY RESOLVES: assuming GCH, either (a) prove that every set mapping $f:\omega_{\omega+1}\to[\omega_{\omega+1}]^{\leq\aleph_\omega}$ with pairwise intersections of size $<\aleph_\omega$ admits a free set of cardinality $\aleph_{\omega+1}$, or (b) construct (under GCH, or show consistent with ZFC+GCH via forcing/inner models, with the metatheory explicit) such a set mapping with no free set of cardinality $\aleph_{\omega+1}$. An independence proof — models of ZFC+GCH deciding it each way — also fully resolves. Machine-checkable (Lean/Coq) proof preferred, else a complete written proof; a computation cannot contribute to closure. ADVANCES: prove the existence of free sets of intermediate cardinality (e.g. $\aleph_\omega$ or every $\aleph_n$) under the stated hypotheses; settle the analogous question at a smaller successor-of-singular test case or under stronger hypotheses (e.g. intersections uniformly bounded below $\aleph_\omega$, or $\square_{\aleph_\omega}$-type principles); or prove the question equivalent to a known PCF or square-principle statement. Deliver the proof file or Lean sources, with all set-theoretic assumptions explicit.