A Machine-Verified Cosmological-Ontological Argument for the Existence of God

We present a machine-verified formal argument for the existence and nature of God, formalized in Isabelle/HOL using a shallow semantic embedding of S5 modal logic. The argument weaves together three traditionally distinct threads — a cosmological argument grounded in the Principle of Sufficient Reason, a Godelian ontological argument based on a positivity predicate, and a causal-structural argument from MaximalCause — into a single unified theory. We establish seven principal result areas: the necessary existence of a Creator, the uniqueness of God, the grounding of morality in the divine nature, the non-contingency of the Creator, divine simplicity, six classical divine attributes, and a formal theodicy dissolving the problem of evil. Crucially, the Principle of Sufficient Reason itself is derived rather than assumed, grounded in a privation theory of non-existence formalized as the Causal Lift Principle. The argument is anchored to physical reality through an empirical premise about the causal structure of the Universe. The modal space is grounded in God as the necessary MaximalCause of all being and all possibility. All proofs are machine-checked by Isabelle's logical kernel. Twenty-five results are derived rather than assumed. The same foundational framework that proves God's existence also explains why evil exists and why God cannot eliminate it without contradiction — the problem of evil is not answered but dissolved.