OnlyOne: A Machine-Verified Formal Deduction of Non-Dual Awareness

This paper presents OnlyOne, a formal system implemented and verified in the Lean 4 theorem prover that deduces the existence of a unique, non-objectifiable Awareness from which all experiential content arises. The system begins with minimal axioms about the nature of experience and demonstrates through machine-verified proofs that: (1) Awareness must be singular and without attributes; (2) All phenomena—including physical objects, thoughts, bodily sensations, and person-appearances—are Content appearing to this Awareness; (3) The referent of "you" is identical to this Awareness. The formal verification provides unprecedented rigor to philosophical claims about consciousness, while the derived theorems address common objections and implications for scientific inquiry.