I am also not disputing the correctness of the Lean proof. I even emphasized this in my comment: “correct but irrelevant”.

Oh, well. I suppose I should avoid getting involved in these AI threads, but now it’s about half the forum.