Axiomatizing projective Hilbert spaces This question arises in connection to trying to take a different (more intrinsic) perspective on the foundations of quantum mechanics, in which projective Hilbert spaces naturally arise, e.g. see Folland, Quantum Field Theory: a Tourist Guide for Mathematicians, section 3.1.
Let $\mathcal{H}$ a (complex) Hilbert space. We then define the associated projective Hilbert space $\mathcal{P(H)}$ as $\mathcal{H}-\{0\}/\mathbb{C}^\times$, i.e. the set of equivalence classes under $\sim$ where $x\sim y$ iff $x = ay$ for some $a \in \mathbb{C}$ nonzero. Then there is a well-defined "ray product", which we will denote by $*$, induced by the inner product on $\mathcal{H}$, which is given by
$$[x] *[y] = \frac{|\langle x,y\rangle|}{\|x\|\|y\|}.$$
Then we can think of this ray product as a function $f : \mathcal{P(H)} \times \mathcal{P(H)} \to [0,1]$, and note that it has some simple properties:

*

*Symmetry: $f(x,y) = f(y,x)$.

*"Definiteness": $f(x,y) =1 \iff x=y$.

*"Linear combination of two orthogonal vectors": if $f(x,y) = 0$ then for any $a,b \in [0,1]$ s.t. $a^2 +b^2 = 1$, there exists $z$ s.t. $f(x,z) = a$ and $f(y,z)=b$.

It seems fairly difficult to think of non-trivial properties of $f$, but there definitely are some, seeming mostly to come from the existence of any linear combination in the Hilbert space.
The question then is whether we can give necessary and sufficient conditions on a function $f: X \times X \to [0,1]$ on some set $X$ to ensure that $X$ arises as a projective Hilbert space for which $f$ is the ray product. Any references or partial progress (e.g. more interesting properties of the ray product) are welcome.
Note: There is a well-known paper by Ashtekar and Schilling that takes projective Hilbert spaces as the fundamental spaces of QM, but they deemphasize this ray product and emphasize more geometric aspects. There are good physical reasons to view the ray product as instead fundamental, as such a natural axiomatization of the ray product would give another route by which one could motivate quantum mechanics.
 A: The paper Metric characterization of elliptic space by Leonard M. Blumenthal answers your question once you recognise that your ray product $[x] * [y]$ (or $f(x,y)$) is equal to $\cos(d(x,y))$ where $d:X\times X \to \mathbb R$ is the metric of a metric space $(X,d)$ which happens to be an elliptic space. The above paper shows what's needed for $(X,d)$ to be an elliptic space in either finite or infinite dimensions. Postulate VI ensures the Cauchy completeness property.
A: This reference on applications of Solèr's theorem appears to answer your question: ORTHOMODULARITY IN INFINITE DIMENSIONS; A
THEOREM OF M. SOLER by Samuel S. Holland Jr.
It axiomatises Hilbert spaces over $\mathbb R, \mathbb C, \mathbb H$ without mentioning real numbers or any analytic concepts. It is then possible (in Section 4) to define projective spaces over these rings in a completely axiomatic way without explicitly mentioning $\mathbb R$. Once again though, you are really asking about elliptic geometry as opposed to projective geometry, so you might need to do some work.
