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

The Universal Generative Principle (\ugp{}) is a deterministic arithmetic framework defined over integer ridges R_n = 2^n - 16. It produces, from first principles and without free parameters, a unique canonical seed---the triple (1,73,823)---whose orbit under the Generative Triple Evolution (\gte{}) map is rigidly determined. We present ugp-lean, a machine-checked formalization of this framework in \lean{} 4 against Mathlib, comprising 51 modules with a strict zero-sorry, zero-custom-axiom policy on the core proof path. \textbf{What makes \ugp{} special, and what this paper proves.} The \ugp{} exhibits three distinct, interlocking properties, each of which we formalize and machine-check: (1) Algebraic…