Proving the topology of the pure state of a qubit in Interv

Because I was curious about what a wave function is, I asked omp to prove something about it.

From some Internet searches, the pure-state space of a qubit is the 2-sphere: the Bloch sphere. Equivalently, the complex projective line is the Riemann sphere, $\mathbf{CP}^1 = S^2$. Before I started this project, I did not know what $\mathbf{CP}^1$ is.

The proof is written in Interv, a small functional language that bootstraps itself and that we have been building for the past month. The proof is written in its cubical type theory. It lives in the interv repository at research/cp1-s2/¹ in three files: pure_state_sphere.ivs, bloch_sphere_equiv.ivs, and real_anisotropy.ivs.

Thoughts

Making Interv and the proof is exciting. Writing this article is not. Now I understand why some people do not like writing research papers.

Mathematics is verifiable by anyone; computation need not be; only some computation counts as mathematics. A machine-checked proof does not rest on trusting the reader’s mathematical knowledge. Much of science and mathematics is built on intuition. Without intuition, proofs become precise and complex. Concepts stack on top of concepts: the integers, then the real numbers, then the topology.

Given enough electricity, if a language model understands something and can achieve it, it will achieve it.

The math behind the proof

This section explains the proof in natural language, for anyone who wants to follow it without reading the code. When I express mathematics, I prefer code, then written notation, then natural language.

A pure qubit state is a ray: a nonzero vector in $\mathbb{C}^2$, considered up to multiplication by a nonzero complex scalar.

The obvious way to turn that into a sphere is to normalise — rescale the spinor so that $|a|^2 + |b|^2 = 1$ — but that does not work. A normalised spinor is a point on the unit 3-sphere inside $\mathbb{C}^2$, and the global phase is still there, so one physical ray corresponds to many points. Dividing out the global phase is the projective step: $S^3 / S^1 = \mathbf{CP}^1 = S^2$ (the Hopf fibration). It is the projective step, not the normalisation step, that lands you on the sphere.

The statement is genuinely about the reals: it depends on anisotropy — that $x^2 + y^2 = 0$ implies $x = y = 0$ — which holds over $\mathbb{R}$ but fails over $\mathbb{C}$ (at $(1 : i : 0 : 0)$, $1 + i^2 = 0$). The correspondence is stereographic projection. Every map is polynomial and uses no division. The proof works by reflection: polynomials in the indeterminates have canonical normal forms, so equality is decidable. Each theorem is a path closed by refl; a genuinely wrong identity is rejected by the checker.

The algebraic correspondence holds over any field of characteristic not equal to 2: both charts, both round-trips, and the chart covering. The two core files — pure_state_sphere.ivs and bloch_sphere_equiv.ivs — assume no postulates. The real version assumes exactly an ordered-field fragment, of which anisotropy is the one non-derivable ingredient. The analytic topological homeomorphism is not machine-checked; it would need the reals of elab/reals.ivs.