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 is included in case anyone wants to know about the proof in natural language. I actually understand the Interv proof more that the English words picked to represent the same mathematical concepts. My preference of expression math is code > written math syntax > natural language.

A pure qubit state is a ray: a nonzero vector in $\mathbb{C}^2$, modulo 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 is wrong. 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). The projective step, not the normalisation step, is what lands you on the sphere.

The statement is genuinely about the reals: it depends on anisotropy, which holds over $\mathbb{R}$ but fails over $\mathbb{C}$. The correspondence is stereographic projection; every map is polynomial, with 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, the chart covering. The core two files assume no postulates. The real version assumes exactly an ordered-field fragment; anisotropy is the one non-derivable ingredient. The analytic topological homeomorphism is not machine-checked; it would need the reals of elab/reals.ivs.