Struct UnitQuaternion 

pub struct UnitQuaternion { /* private fields */ }

Unit quaternion representing an element of SU(2)

Quaternion q = w + xi + yj + zk where w² + x² + y² + z² = 1

Geometric Interpretation

Every unit quaternion represents a rotation in 3D space:

• Rotation by angle θ around axis n̂ = (nx, ny, nz): q = cos(θ/2) + sin(θ/2)(nx·i + ny·j + nz·k)

⚠️ Important: Double Cover Property

q and -q represent the SAME rotation but DIFFERENT quantum states:

• Both rotate 3D vectors identically (v → q·v·q⁻¹ = (-q)·v·(-q)⁻¹)
• But q ≠ -q as SU(2) group elements
• Consequence: Fermions change sign under 2π rotation (ψ → -ψ)

This is NOT a numerical issue or degeneracy - it’s fundamental topology!

Relation to SU(2) Matrix

q = w + xi + yj + zk corresponds to SU(2) matrix:

U = [[ w + ix,  -y + iz],
     [ y + iz,   w - ix]]

Note: -q gives matrix -U, which acts identically on vectors but represents a different element of SU(2) (relevant for spinors/fermions).

Implementations

impl UnitQuaternion

pub fn w(&self) -> f64

Get the real (scalar) component.

pub fn x(&self) -> f64

Get the imaginary i component.

pub fn y(&self) -> f64

Get the imaginary j component.

pub fn z(&self) -> f64

Get the imaginary k component.

pub fn components(&self) -> (f64, f64, f64, f64)

Get all components as a tuple (w, x, y, z).

pub fn to_array(&self) -> [f64; 4]

Get all components as an array [w, x, y, z].

impl UnitQuaternion

pub fn identity() -> Self

Identity element: q = 1

pub fn new(w: f64, x: f64, y: f64, z: f64) -> Self

Create from components (automatically normalizes to unit quaternion)

Returns identity if input norm < NORM_EPSILON (degenerate case).

pub fn from_axis_angle(axis: [f64; 3], angle: f64) -> Self

Create from axis-angle representation

Arguments

• axis - Rotation axis (nx, ny, nz), will be normalized
• angle - Rotation angle in radians

Returns

Unit quaternion q = cos(θ/2) + sin(θ/2)(nx·i + ny·j + nz·k)

pub fn to_axis_angle(&self) -> ([f64; 3], f64)

Extract axis and angle from quaternion

Returns

(axis, angle) where axis is normalized and angle ∈ [0, 2π]

pub fn rotation_x(theta: f64) -> Self

Rotation around X-axis by angle θ

pub fn rotation_y(theta: f64) -> Self

Rotation around Y-axis by angle θ

pub fn rotation_z(theta: f64) -> Self

Rotation around Z-axis by angle θ

pub fn conjugate(&self) -> Self

Quaternion conjugate: q* = w - xi - yj - zk

For unit quaternions: q* = q⁻¹ (inverse)

pub fn inverse(&self) -> Self

Quaternion inverse: q⁻¹

For unit quaternions: q⁻¹ = q*

pub fn norm_squared(&self) -> f64

Norm squared: |q|² = w² + x² + y² + z²

Should always be 1 for unit quaternions

pub fn norm(&self) -> f64

Norm: |q| = sqrt(w² + x² + y² + z²)

Should always be 1 for unit quaternions

pub fn normalize(&self) -> Self

Renormalize to unit quaternion (fix numerical drift)

pub fn distance_to_identity(&self) -> f64

Distance to identity (geodesic distance on S³)

d(q, 1) = 2·arccos(|w|)

This is the rotation angle in [0, π]

pub fn distance_to(&self, other: &Self) -> f64

Geodesic distance to another quaternion

d(q₁, q₂) = arccos(|q₁·q₂|) where · is quaternion dot product

pub fn slerp(&self, other: &Self, t: f64) -> Self

Spherical linear interpolation (SLERP)

Interpolate between self and other with parameter t ∈ [0,1] Returns shortest path on S³

pub fn exp(v: [f64; 3]) -> Self

Exponential map from Lie algebra 𝔰𝔲(2) to group SU(2)

Given a vector v = (v₁, v₂, v₃) ∈ ℝ³ (Lie algebra element), compute exp(v) as a unit quaternion.

Formula: exp(v) = cos(|v|/2) + sin(|v|/2)·(v/|v|)

pub fn log(&self) -> [f64; 3]

Logarithm map from group SU(2) to Lie algebra 𝔰𝔲(2)

Returns vector v ∈ ℝ³ such that exp(v) = q

Formula: log(q) = (θ/sin(θ/2))·(x, y, z) where θ = 2·arccos(w)

pub fn to_matrix(&self) -> [[Complex64; 2]; 2]

Convert to SU(2) matrix representation (for compatibility)

Returns 2×2 complex matrix: U = [[ w + ix, -y + iz], [ y + iz, w - ix]]

pub fn from_matrix(matrix: [[Complex64; 2]; 2]) -> Self

Create from SU(2) matrix

Expects matrix [[α, -β*], [β, α*]] with |α|² + |β|² = 1

pub fn rotate_vector(&self, v: [f64; 3]) -> [f64; 3]

Act on a 3D vector by conjugation: v’ = qvq*

This is the rotation action of SU(2) on ℝ³ Identifies v = (x,y,z) with quaternion xi + yj + zk

Uses the direct formula (Rodrigues) for efficiency: v’ = v + 2w(n×v) + 2(n×(n×v)) where n = (x,y,z)

pub fn verify_unit(&self, tolerance: f64) -> bool

Verify this is approximately a unit quaternion

pub fn to_rotation_matrix(&self) -> [[f64; 3]; 3]

Construct the 3×3 rotation matrix corresponding to this unit quaternion.

Returns the SO(3) matrix R such that R·v = rotate_vector(v) for all v ∈ ℝ³.

Lean Correspondence

This is the Rust counterpart of toRotationMatrix in OrthogonalGroups.lean. The Lean proofs establish:

• toRotationMatrix_orthogonal_axiom: R(q)ᵀ·R(q) = I
• toRotationMatrix_det_axiom: det(R(q)) = 1
• toRotationMatrix_mul_axiom: R(q₁·q₂) = R(q₁)·R(q₂)
• toRotationMatrix_neg: R(-q) = R(q)

Trait Implementations

impl Clone for UnitQuaternion

fn clone(&self) -> UnitQuaternion

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for UnitQuaternion

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Mul for UnitQuaternion

type Output = UnitQuaternion

The resulting type after applying the * operator.

fn mul(self, rhs: Self) -> Self

Performs the * operation.

impl MulAssign for UnitQuaternion

fn mul_assign(&mut self, rhs: Self)

Performs the *= operation.

impl PartialEq for UnitQuaternion

fn eq(&self, other: &UnitQuaternion) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for UnitQuaternion

impl StructuralPartialEq for UnitQuaternion