Struct VerifiedMultivector 

pub struct VerifiedMultivector<T, const P: usize, const Q: usize, const R: usize>
where
    T: Float + Zero + One,
{ /* private fields */ }

A verified multivector with compile-time signature guarantees

This structure ensures at the type level that:

1. The signature is fixed and consistent
2. Operations preserve algebraic laws
3. Dimension bounds are respected

Implementations

impl<T, const P: usize, const Q: usize, const R: usize> VerifiedMultivector<T, P, Q, R>

where T: Float + Zero + One,

pub const DIM: usize

The total dimension of the algebra

pub const BASIS_SIZE: usize

The number of basis blades (2^n)

pub fn new(coefficients: Vec<T>) -> Result<Self, &'static str>

Create a new verified multivector from coefficients

Type Invariants

• Coefficients array must have exactly 2^(P+Q+R) elements
• Signature is encoded at type level and cannot be violated

pub fn scalar(value: T) -> Self

Create a scalar multivector

pub fn basis_vector(index: usize) -> Result<Self, &'static str>

Create a basis vector e_i

Type Safety

The index is bounds-checked against the signature dimensions

pub fn is_scalar(&self) -> bool

Check if this is a pure scalar

pub fn grade(&self) -> usize

Compute the grade (highest non-zero grade component)

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

Addition of multivectors (same signature enforced by types)

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

Geometric product with compile-time signature matching

Mathematical Properties (verified by Creusot when enabled)

• Associativity: (AB)C = A(BC)
• Distributivity: A(B+C) = AB + AC
• Identity: 1A = A1 = A

Trait Implementations

impl<T, const P: usize, const Q: usize, const R: usize> Clone for VerifiedMultivector<T, P, Q, R>

where T: Float + Zero + One + Clone,

fn clone(&self) -> VerifiedMultivector<T, P, Q, R>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<T, const P: usize, const Q: usize, const R: usize> Debug for VerifiedMultivector<T, P, Q, R>

where T: Float + Zero + One + Debug,

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

Formats the value using the given formatter.