ugp-lean: A Machine-Checked Formalization of the Universal Generative Principle | Synapse