A Lean 4 + Mathlib formalization of uncertified DAG consensus (Mysticeti-style): machine-checked safety, liveness from eventual DAG synchrony, and five further arcs