Maximum edges in a graph with no two edge-disjoint cycles on the same vertex set (Erdős #585)

What is the maximum number of edges that a graph on $n$ vertices can have if it does not contain two edge-disjoint cycles with the same vertex set? Here two cycles are edge-disjoint if they share no edge, and they have the same vertex set if they pass through exactly the same vertices (the forbidden configuration is thus a vertex set $S$ carrying two cycles, each spanning all of $S$, with no common edge). Determine the growth order of this extremal function.

Acceptance. FULLY RESOLVES: matching upper and lower bounds for the extremal function up to a constant factor (an asymptotic determination of its growth order), each with a complete proof — machine-checkable (Lean/Coq) preferred, otherwise a full written proof; constructions must come with proofs that they avoid the forbidden configuration. A finite computation alone cannot close the asymptotic question. ADVANCES: (a) an upper bound with a strictly smaller growth rate than the best upper bound stated in the background (currently $n(\log n)^{O(1)}$ — e.g. an explicit small power of $\log n$, or $n\cdot(\log n)^{o(1)}$), with proof; (b) a construction strictly beating the $n\log\log n$ lower bound stated in the background, with a verifiable proof of correctness; (c) exact values of the extremal function for small $n$ (with the extremal graphs), computed by exhaustive isomorph-free enumeration and accompanied by the search code and an exhaustiveness certificate — enough values to make the initial segment of the sequence citable; (d) sharpening the dependence $c_k$ or the exponent $C$ in the $k$-cycle strengthening, with proof. Deliver the proof file (or compiling Lean sources), or the construction plus verification, or the enumeration code with the certified table of exact values.