feat(QuantumInfo): angle-parameterized qubit ket for Pancharatnam connection

[wock9000]

Summary

Define qubitKet α θ representing cos(α/2)|0⟩ + e^{iθ}sin(α/2)|1⟩ — the standard angle-parameterized qubit state mapping to blochPoint α θ on the Bloch sphere.

Prove dot_qubitKet: the inner product of two such states in closed half-angle form,

〈ψ₁‖ψ₂〉 = cos(α₁/2)cos(α₂/2) + e^{i(θ₂-θ₁)}sin(α₁/2)sin(α₂/2)

which is the computational core for connecting the Bargmann invariant to the solid angle (Pancharatnam's theorem).

New definitions and results

Name	Kind	Description
qubitKet	def	Qubit ket from Bloch sphere angles (α, θ)
qubitKet_apply_zero	@[simp] lemma	Component 0: ↑(cos(α/2))
qubitKet_apply_one	@[simp] lemma	Component 1: exp(iθ) · ↑(sin(α/2))
dot_qubitKet	lemma	Inner product in half-angle form

Design notes

• Uses Ket (Fin 2) directly rather than importing Qubit (which pulls in the full Channels stack). The parameterization is identical to blochPoint from BlochSphere.lean.
• The raw vector is factored into a private def qubitKetVec to prevent simp [qubitKet] from unfolding through the normalization proof term.
• Single import: BlochSphere, which transitively provides Braket, BargmannInvariant, and Mathlib's complex analysis.

Build

74 lines, zero warnings from this file, zero errors. Tested on v4.29.1 after rebasing onto current master (includes #1134).

References

S. Pancharatnam, Generalized theory of interference, and its applications, Proc. Indian Acad. Sci. A 44, 247–262 (1956)

[jstoobysmith]

I think the stuff in this file is maybe more appropriate for the Braket or Qubit file