The Borsuk number of the complex projective plane is nine

For the rank-one projector realization of the complex projective plane in the eight-dimensional affine space of trace-one Hermitian matrices with the Frobenius metric, we prove diameter sqrt(2) and Borsuk number exactly nine. The lower bound covers arbitrary subsets. A covariant perturbation of the nine Hesse rays, controlled by a uniform two-trio estimate in complex neighborhoods, yields nine compact sets of strictly smaller diameter and nine Fubini–Study balls of radius below pi/4 covering the whole space. This attains d+1 in dimension eight. The accompanying Lean development formalizes supporting scalar inequalities and complex identities, not the full geometric and topological theorem.