Can a graph with $\epsilon n^2$ edges be $n$-coloured so every $C_4$ is rainbow? (Erdős #810)

Does there exist a constant $\epsilon>0$ such that, for all sufficiently large $n$, there is a graph $G$ on $n$ vertices with at least $\epsilon n^2$ edges whose edges can be coloured with $n$ colours so that every $4$-cycle $C_4$ in $G$ receives $4$ distinct colours (a rainbow $C_4$)? Equivalently, writing $\chi_S(n,e,H)$ for the smallest number of colours $r$ admitting an edge-colouring of some graph with $n$ vertices and $e$ edges in which every copy of $H$ is rainbow, does there exist $\epsilon>0$ with $$\chi_S(n,\epsilon n^2,C_4)\leq n$$ for all large $n$?

Acceptance. FULLY RESOLVES: a complete proof settling whether there is a fixed $\epsilon>0$ with $\chi_S(n,\epsilon n^2,C_4)\leq n$ for all large $n$ — either an explicit family of $n$-vertex graphs ($n\to\infty$) with $\geq\epsilon n^2$ edges together with an $n$-colouring proven to make every $C_4$ rainbow, or a proof that no such $\epsilon$ exists (i.e. $\chi_S(n,\epsilon n^2,C_4)/n\to\infty$ for every fixed $\epsilon>0$); a machine-checkable proof (Lean/Coq) is preferred, otherwise a full written proof with all steps. ADVANCES: (a) determine the order of $g(n;7,4)$ — in particular prove $g(n;7,4)=o(n^2)$ or exhibit $g(n;7,4)\gg n^2$ — with proof; (b) prove new upper or lower bounds on $\chi_S(n,\epsilon n^2,C_4)$ strictly improving what the background records; or (c) for a new record $n$, compute $\chi_S(n,e,C_4)$ exactly at $e\approx\epsilon n^2$ with a reproducible exhaustive/ILP certificate extending the tabulated evidence. Deliver the proof file, or the construction plus colouring and verification code, or the search code plus certified values.