Monochromatic sets in strictly Δ-regressive colourings

For every ordinal θ > ω, every Δ-regressive colouring c: [2θ]2 → θ has a monochromatic four-element set of a natural-number colour. Here Δ(x,y) is the first coordinate at which x and y differ, and regressivity means c(x,y) < Δ(x,y) whenever Δ(x,y) > 0. This answers the four-element-set part of Problem 5.2 of Lambie-Hanson and Soukup. The proof follows a nested sequence of full binary cones, successively excluding small colours. We give an explicit colouring on 2ω+1 with no monochromatic five-element set, showing that the four-element conclusion is sharp at this length. At length ω, we prove that every Δ-regressive colouring into ω has a monochromatic triangle. This contradicts Observation 2.1 of the arXiv v2 version of the same paper; we also give a three-point counterexample to its displayed colouring. All proofs are elementary and are carried out in ZFC. This English preprint includes complete proofs, attribution of the predecessor argument and maximality lemma, and disclosure of AI-generated mathematical content. The comparison concerns arXiv:2002.02480v2; no claim is made about whether the journal version has the same error. The manuscript has undergone AI-assisted proof and editorial review, not independent expert review. Version v2 adds a Lean 4.30.0 formalization of the numbered results, their supporting lemmas, the normalized reduction, the finite-terminal-colour variation, and the explicit boundary examples. The maximality lemma is proved internally. The complete repository checks passed locally and on GitHub for commit eb0611f64f1305e9faf51e4f12f06b4a00ca729e; the checks include expanded statements, source hashes, module coverage, and a transitive kernel axiom audit. The only permitted logical axioms are propext, Classical.choice, and Quot.sound. The open questions and external literature discussion are outside the formalization claim. Files contain the seven-page article PDF, its LaTeX source, and a complete Lean repository snapshot with pinned dependencies and verification evidence. Lean formalization and coverage map | Successful Lean verification run.