The space of quantum states carries a metric and a rotation that agree with each other. That agreement is what makes its volume canonical rather than arbitrary.
isFubiniStudyKahlerThe space of quantum states has three structures that could each have been independent: a way of measuring distance, a way of measuring area, and a quarter-turn operation coming from the complex numbers. In fact they lock together, each recoverable from the other two. A space where they lock together in this way has a volume nothing else has to supply, which is why the ruler used throughout this programme is not an extra ingredient.
This underwrites the claim that the typicality measure is geometric rather than chosen. What is proved here is the pointwise compatibility on the tangent model: the quarter-turn squares to minus one, the area form is the metric composed with it and vice versa, the form is invariant under the quarter-turn on both slots, and pairing a vector with its own turn returns its squared length. Flat closedness is likewise proved on the tangent model.
With g the real part of the inner product, omega the imaginary part, and J multiplication by i, the Fubini-Study Kahler compatibility holds pointwise: J^2 = -1, omega = g composed with J, g = omega composed with J, omega is of type (1,1), and omega(u, Ju) = the squared norm of u. Proved axiom-free. Scope to disclose, and it is load-bearing: the MANIFOLD residual is NOT formalised. Closedness and the top-power identity omega^(N-1)/(N-1)! = the Fubini-Study measure ON the projective space itself await a manifold differential-form API the proof assistant does not yet carry. Kahler differential geometry must therefore not be described as load-bearing here; the pointwise core is what the corpus owns.
Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.