Determine the average order of $g_k(n)$, the factorial-excess with $a_1!\cdots a_k!\mid n!$ (Erdős #400)

For an integer $k\ge 2$ and a positive integer $n$, let $g_k(n)$ be the maximum value of $(a_1+\cdots+a_k)-n$ over all nonnegative integers $a_1,\ldots,a_k$ satisfying $a_1!\cdots a_k!\mid n!$. (Taking $a_1=n$ and $a_2=\cdots=a_k=1$ shows $g_k(n)\ge k-1$, since $0!=1!=1$.) Prove or disprove that there is a constant $c_k>0$ with $$\sum_{n\le x} g_k(n)\sim c_k\, x\log x,$$ and decide whether there is a constant $c_k$ such that for almost all $n<x$ one has $$g_k(n)=c_k\log x + o(\log x).$$

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, otherwise a full written proof with all steps) that, for each fixed $k\ge 2$ (or a stated range of $k$), $\sum_{n\le x} g_k(n)\sim c_k\, x\log x$ with the constant $c_k$ explicitly identified or characterised, together with a resolution of the normal-order statement ($g_k(n)=c_k\log x+o(\log x)$ for almost all $n<x$) — OR a disproof of either asymptotic. ADVANCES (each independently checkable): (a) a rigorous improvement to the implied constant in the known bound $g_k(n)\ll_k\log n$, or a matching lower bound $g_k(n)\gg_k\log n$ for infinitely many $n$, in either case strictly better than the best bound stated in the background, with proof; (b) a reproducible exact computation of $g_k(n)$ for all $n\le X$ at a new record height $X$, delivered with the search program and an exhaustiveness certificate, yielding numerical estimates of $c_k$ and of the empirical distribution of $g_k(n)/\log n$; (c) a proof of the average-order or normal-order claim conditional on a clearly stated hypothesis. Deliver the proof file, or the search code plus attained height and tabulated estimates.