Ok, I think I have this by a sequence of reductions: First, prove the case where our proper map is $P^n_A\to A$. In this case, we can directly apply absolute Noetherian approximation to the base $A$, so we're done by Giraud and 3-for-2. Then, we also have the case where $X$ is projective over $A$ because proper basechange for closed immersions is obvious (using 2-topos theory, for example).

Since projective maps now satisfy basechange for constructible 1-sheaves, we can show that projective surjective maps are universal effective descent maps for constructible 1-sheaves (universal effective descent for constructible 0-sheaves implies universal descent for constructible 1-sheaves, and projective base-change for constructible 1-sheaves and universal descent for constructible 1-sheaves together imply universal effective descent for constructible 1-sheaves).

Now in the general case, apply Chow's lemma to find a proper cover $X^\prime\to X$ by an $X^\prime,$ which embeds as a closed subscheme of $P^n_A$. We then also see that $X^\prime \to P^n_A \times_A X = P^n_X$ is also a closed immersion, so now use the theorem for the projective map $X^\prime \to A$ and use effective descent for the map $X^\prime \to X$, so we're done.

The key point seems to be that you have to apply Noetherian approximation early on rather than later on.

Edit/Warning: I just realized that I accidentally put $A$ here everywhere instead of $Y$. Since I don't want to bother rewriting the comments I left below, I'm just noting this in advance.

Ok, I think I have this by a sequence of reductions: First, prove the case where our proper map is $P^n_A\to A$. In this case, we can directly apply absolute Noetherian approximation to the base $A$, so we're done by Giraud and 3-for-2. Then, we also have the case where $X$ is projective over $A$ because proper basechange for closed immersions is obvious (using 2-topos theory, for example).

Since projective maps now satisfy basechange for constructible 1-sheaves, we can show that projective surjective maps are universal effective descent maps for constructible 1-sheaves (universal effective descent for constructible 0-sheaves implies universal descent for constructible 1-sheaves, and projective base-change for constructible 1-sheaves and universal descent for constructible 1-sheaves together imply universal effective descent for constructible 1-sheaves).

Now in the general case, apply Chow's lemma to find a proper cover $X^\prime\to X$ by an $X^\prime,$ which embeds as a closed subscheme of $P^n_A$. We then also see that $X^\prime \to P^n_A \times_A X = P^n_X$ is also a closed immersion, so now use the theorem for the projective map $X^\prime \to A$ and use effective descent for the map $X^\prime \to X$, so we're done.

The key point seems to be that you have to apply Noetherian approximation early on rather than later on.

Ok, I think I have this by a sequence of reductions: First, prove the case where our proper map is $P^n_A\to A$. In this case, we can directly apply absolute Noetherian approximation to the base $A$, so we're done by Giraud and 3-for-2. Then, we also have the case where $X$ is projective over $A$ because proper basechange for closed immersions is obvious (using 2-topos theory, for example).

Since projective maps now satisfy basechange for constructible 1-sheaves, we can show that proper surjective maps are universal effective descent maps for constructible 1-sheaves (universal effective descent for constructible 0-sheaves implies universal descent for 1-sheaves, and base-change for 1-sheaves and universal descent for 1-sheaves together imply universal effective descent for 1-sheaves).

Now in the general case, apply Chow's lemma to find a proper cover $X^\prime\to X$ by an $X^\prime,$ which embeds as a closed subscheme of $P^n_A$. We then also see that $X^\prime \to P^n_A \times_A X = P^n_X$ is also a closed immersion, so now use the theorem for the projective map $X^\prime \to A$ and use effective descent for the map $X^\prime \to X$, so we're done.

The key point seems to be that you have to apply Noetherian approximation early on rather than later on.

Ok, I think I have this by a sequence of reductions: First, prove the case where our proper map is $P^n_A\to A$. In this case, we can directly apply absolute Noetherian approximation to the base $A$, so we're done by Giraud and 3-for-2. Then, we also have the case where $X$ is projective over $A$ because proper basechange for closed immersions is obvious (using 2-topos theory, for example).

Since projective maps now satisfy basechange for constructible 1-sheaves, we can show that projective surjective maps are universal effective descent maps for constructible 1-sheaves (universal effective descent for constructible 0-sheaves implies universal descent for constructible 1-sheaves, and projective base-change for constructible 1-sheaves and universal descent for constructible 1-sheaves together imply universal effective descent for constructible 1-sheaves).

Now in the general case, apply Chow's lemma to find a proper cover $X^\prime\to X$ by an $X^\prime,$ which embeds as a closed subscheme of $P^n_A$. We then also see that $X^\prime \to P^n_A \times_A X = P^n_X$ is also a closed immersion, so now use the theorem for the projective map $X^\prime \to A$ and use effective descent for the map $X^\prime \to X$, so we're done.

The key point seems to be that you have to apply Noetherian approximation early on rather than later on.