Erdős–Surányi product divisibility: is $g(n)\leq(2+o(1))n$? (Erdős #708)

Let $g(n)$ be minimal such that for any $A\subseteq[2,\infty)\cap\mathbb{N}$ with $\lvert A\rvert=n$ and any set $I$ of $\max(A)$ consecutive integers there exists $B\subseteq I$ with $\lvert B\rvert=g(n)$ such that $$\prod_{a\in A} a \;\Big|\; \prod_{b\in B} b.$$ Is it true that $g(n)\leq(2+o(1))n$? Or perhaps even $g(n)\leq 2n$?

Acceptance. FULLY RESOLVES (proof-shaped): a complete rigorous proof — a Lean/Coq formalisation preferred, otherwise a full written proof — that $g(n)\leq(2+o(1))n$ (or the sharper $g(n)\leq 2n$), or a disproof exhibiting sequences $A$ that force $g(n)$ larger; equivalently, an asymptotic formula for $g(n)$ with proof. ADVANCES: (a) determine $g(n)$ exactly for some $n$ beyond the current record (only $g(2)=2$ and $g(3)=4$ are known), with a machine-checkable certificate of both the extremal $A$ and the matching upper bound; (b) improve the lower bound $g(n)\geq(2-o(1))n$ stated in the background via a better construction, with proof; or (c) prove any upper bound of the form $g(n)\leq Cn$ for an explicit constant $C$, with proof (no linear upper bound is currently stated). Deliver the proof, the certified exact values plus search code, or the improved construction.