Also, a collision on single-sha256 would imply a collision of double-sha256 right off the bat, since the inputs to the second round would be matching. But as you say, a collision attack doesn't do much to BTC mining.

Thanks, you're right. My "it is possible" is doing some heavy lifting there :). We've found theorems (stated in the paper) that carry through 64 rounds, so it is possible that theorems might carry through the full 128 rounds of double-SHA256. Bitcoin's proof-of-work is indeed a "partial second preimage", and constraints a certain number of leading zeros, i.e. a certain number of set bits. It's possible (there we go again) that this could leave enough wiggle room for large algabraic solvers like kissat to satisfy a large number of clauses about them. So far nobody is doing that, and ASICs are very simplistic. However, we are not making any claims about preimage attacks in this paper!