Existence as Distinguishability: Quantum Mechanics from Finite Graded Equality

We derive finite-dimensional quantum mechanics from a single ontological principle, that \emph{existence is constituted by distinguishability}, together with two structural commitments: finite capacity $N$ (parametric input) and self-referential consistency (SRC, a closure schema with two equivalent forms, operational and information-theoretic). SRC unpacks into eight derived structural conditions; structural unambiguity (S5) completes the hierarchy, uniquely selecting the Born rule as the geometric/probabilistic closure. The graded distinguishability kernel $K(x,y) \in [0,1]$ realises both axioms, with a state constituted by its $K$-profile against all others. For each $N \geq 3$, the unique distinguishability space is $(\mathbb{C} P^{N-1}, K)$ with $K(\psi,\phi) = 1 - |\langle\psi|\phi\rangle|^2$, from which complex coefficients, the Born rule $p_k = |c_k|^2$, unitary dynamics, and tensor-product composition all follow. Indeterminism is forced by capacity overflow; alternatives (e.g. Bohmian mechanics) are classified rather than refuted. Standard QM is the $N \to \infty$ limit; finite $N$ is the only free parameter. The algebraic spine is machine-checked in Lean 4 modulo five imported classical theorems and the existence direction of Stone's theorem; the Appendix states the verification scope.