Dense subgraphs in which every two edges lie on a short cycle: the Duke–Erdős–Rödl problem (Erdős #584)

Let $G$ be a graph with $n$ vertices and $\delta n^2$ edges (here $X \gg Y$ means $X \ge cY$ for an absolute constant $c > 0$, uniformly in $\delta$ and $n$). Are there subgraphs $H_1, H_2 \subseteq G$ such that: (1) $H_1$ has $\gg \delta^3 n^2$ edges, every two edges of $H_1$ are contained in a common cycle of length at most $6$, and moreover any two edges of $H_1$ sharing a vertex lie on a common cycle of length $4$; and (2) $H_2$ has $\gg \delta^2 n^2$ edges and every two edges of $H_2$ are contained in a common cycle of length at most $8$? The bounds must be uniform in $\delta$; the substantive regime is $\delta = n^{-c}$ for fixed $c > 0$.

Acceptance. FULLY RESOLVES: a complete proof of both statements (1) and (2) with the stated exponents, uniform in $\delta$ (machine-checkable Lean/Coq preferred, else a full written proof with all steps); OR a disproof of either statement: an explicit family of graphs $G_n$ with $\delta_n n^2$ edges together with a proof that every subgraph with the required edge count contains two edges lying on no common cycle of the required length. A finite computation alone cannot settle this asymptotic question. ADVANCES: (a) proving statement (1) with any exponent strictly better than the $\delta^5$ of [DER84] stated in the background (e.g. $\delta^4$), uniformly in $\delta$, with proof; (b) extending the density range for statement (2) beyond the best stated in the background (currently $\delta \ge n^{-1/3}$, Li), to a strictly wider range, or establishing statement (1) with the sharp $\delta^3$ exponent including the adjacent-edge length-$4$ cycle condition in that range, with proof; (c) proving either statement in the model regime $\delta = n^{-c}$ for some explicit $c > 0$ where it is currently unknown; (d) a certified counterexample restricted to one of the two statements as formulated. Deliver the proof file (or compiling Lean sources), or the construction plus its verification argument.