Just a nitpick, you only proved $HC$ is correct about $\Sigma_1$ sentences, not $\Sigma_1$ formulae. Not that it really matters, since Shoenfield absoluteness can be relativized to a real (and therefore any element in $HC,$ I think), so the same proof carries through.

Wow, it's surprising to me that statement 1, which is a theorem in pretty much every textbook, is always stated with an unnecessary assumption. Maybe that's just for simplicity of proof, since this theorem is usually earlier than the sections on forcing and well-founded trees.

It is a theorem that if $V \models ZF+DC,$ then $\Sigma_1$ sentences are downward absolute to $L.$ This is because $ZF+DC \vdash HC \prec_1 V,$ so any $\Sigma_1$ sentence is equivalent to a $\Sigma_1^{HC}$ sentence, which is equivalent to a $\Sigma_2^1$ sentence, which is downward absolute to $L$ by Shoenfield absoluteness. The point of this question is determining whether we can get rid of the use of DC in these arguments.

Asaf, the point is to prove downwards absoluteness. Joel, the latter. Each of these three claims are all relativized to $M,$ under the hopes that they can be proven from ZF alone.

Alright duly noted.