Thank you for bringing this up pfdietz. No, not defective. The Lean proofs behind both are machine-checked and unchanged. I withdrew them over framing, not correctness.

1) For #129 a couple people pointed out that the report was very confusing. And I agree. So I'm currently attempting to improve it.

2) For #130, a person pointed it out as being a partial solution. This seems correct, so I'm currently working on making it fully end to end.

These are put out as "proposed solutions" for the mathematics community to scrutinize, and the scrutiny worked exactly like it should. Happy to take any feedback and make them better.