Projective Interior Probability Fibers

Abstract

Squared amplitudes on complex projective space have torus-shaped interior fibers.

Theorem 1.1 (Interior projective probability fibers are tori).

$$\begin{gathered} \forall n\in \mathbb{N},p\in \mathrm{int}({\Delta }_n), \\ (\forall i,p_i>0)\Rightarrow \\ \mathrm{Bijective}(\mathrm{relativePhaseCoordinates}\left(p\right):\{[psi]\in C{P}^n\mid q_B([psi])=p\}\to T^n). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/ProjectiveInteriorProbabilityFiber.projective_interior_probability_fiber_equiv_torus (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix the standard basis on the complex vector space with n plus one coordinates. The public state carrier is its Mathlib projectivization, and the basis-probability map sends any nonzero representative to its coordinatewise squared amplitudes divided by their total.

For a strictly positive probability vector, every representative in the fiber has nonzero coordinates. Scaled affine ratios against coordinate zero therefore have squared norm one and define n relative circle phases.

The inverse uses amplitudes whose positive magnitudes are the square roots of the prescribed probabilities, fixes the reference phase to one, and inserts the n relative phases. Direct representative computations prove both inverse laws on the projective fiber.

References

• Truth anchor: D5/S3/Quantum/Fibers/ProjectiveInteriorProbabilityFiber.projective_interior_probability_fiber_equiv_torus
• Dependency: D5/S3/Quantum/Fibers/InteriorProbabilityPhaseFiber