contracts.cppm File Reference

Rank-nullity and matrix-structural compile-time contracts. More...

#include <concepts>
#include <cstddef>
#include <functional>
#include <type_traits>
#include <utility>
import dedekind.algebra;

Include dependency graph for contracts.cppm:

Classes
struct	dedekind::linear_algebra::StaticRankNullity< AmbientDimension, Rank >
	Convenience compile-time carrier for finite-dimensional witnesses. More...
struct	dedekind::linear_algebra::ColumnOrientation
	Tag for column-oriented 1-tensors (vectors in the usual sense). More...
struct	dedekind::linear_algebra::RowOrientation
	Tag for row-oriented 1-tensors (covectors, linear functionals). More...
struct	dedekind::linear_algebra::dual_orientation< ColumnOrientation >
struct	dedekind::linear_algebra::dual_orientation< RowOrientation >

Concepts
concept	dedekind::linear_algebra::RankNullityWitness
	Static witness for the rank-nullity identity.
concept	dedekind::linear_algebra::LinearOperatorContract
	Minimal contract for finite-dimensional linear operator carriers.
concept	dedekind::linear_algebra::HasDimensionCount
	A carrier exposing a compile-time dimension count (axes or slots).
concept	dedekind::linear_algebra::HasOrientation
	A carrier that declares whether it is a column or a row.
concept	dedekind::linear_algebra::IsColumnVector
	A column vector: an IsSemimodule with ColumnOrientation and a finite dimension. "A matrix column is a (semimodule) vector" — every column_type on an IsMatrix carrier models this. Over a ring the carrier further satisfies dedekind::algebra::IsModule; over a dioid (MaxPlus) it does not, and none is asked.
concept	dedekind::linear_algebra::IsCovector
	A row vector / covector: the RowOrientation twin of IsColumnVector — an IsSemimodule row.
concept	dedekind::linear_algebra::HasMatrixShape
	A matrix carries two dimensionalities: row count and column count.
concept	dedekind::linear_algebra::HasColumnType
	A matrix exposes its columns as a concrete vector carrier.
concept	dedekind::linear_algebra::HasRowType
	A matrix exposes its rows as a concrete covector carrier.
concept	dedekind::linear_algebra::HasColumnDecomposition
	A matrix can be viewed as the horizontal concatenation of its column vectors.
concept	dedekind::linear_algebra::HasRowDecomposition
	A matrix can be viewed as the vertical concatenation of its row vectors.
concept	dedekind::linear_algebra::IsMatrix
	The structural-matrix slogan-pack: shape + column/row types + both decompositions.
concept	dedekind::linear_algebra::IsMatrixSubmoduleLike
	Matrices over a ring form at least a submodule-like carrier.
concept	dedekind::linear_algebra::IsMatrixAsModule
	The strict "sometimes a module" witness.
concept	dedekind::linear_algebra::HasMatrixMultiplication
	Square-matrix multiplication: M × M → M.
concept	dedekind::linear_algebra::HasTranspose
	A matrix carrier equipped with a transpose operation.
concept	dedekind::linear_algebra::HasInvolutiveTranspose
	Transpose is its own inverse at the type level: decltype((a.transpose()).transpose()) is M.
concept	dedekind::linear_algebra::IsTransposeDualPair
	V and Covec are dual under transpose: V → Covec and Covec → V, with both round-trips returning the original type.
concept	dedekind::linear_algebra::IsMatrixOverFieldRingLike
	Matrices over a field carry at least a ring structure plus transpose.
concept	dedekind::linear_algebra::HasMultiplicativeInverse
	A matrix carrier with a closed-form inverse operation.
concept	dedekind::linear_algebra::IsInvertibleMatrixOverField
	A matrix over a field that carries ring-like structure plus an .inverse() operation.
concept	dedekind::linear_algebra::IsOrthogonalMatrixCarrier
	Carries the operations under which the orthogonality law Mᵀ · M = I makes sense.
concept	dedekind::linear_algebra::MatchesAdditiveShape
	Two matrix-like carriers can be added iff they share shape and scalar type.
concept	dedekind::linear_algebra::MatchesMultiplicativeShape
	Two matrix-like carriers can be composed iff the inner dimensions agree: A::column_count == B::row_count and the scalar types match.
concept	dedekind::linear_algebra::HasConformingMatrixAddition
	A and B support shape-conformant addition, and the result has the same shape and scalar type.
concept	dedekind::linear_algebra::HasConformingMatrixMultiplication
	A and B support shape-conformant multiplication, and the result has shape A::row_count × B::column_count.
concept	dedekind::linear_algebra::IsMatrixAlgebra
	Umbrella concept bundling all 9 matrix slogans for square matrices over a field.

Typedefs
template<typename O>
using	dedekind::linear_algebra::dual_orientation_t = typename dual_orientation<O>::type

Detailed Description

Rank-nullity and matrix-structural compile-time contracts.

@partition :contracts

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

Two families of contracts live in this partition:

1. Rank-nullity — historical scope: RankNullityWitness, StaticRankNullity, LinearOperatorContract.
2. Matrix-structural concepts encoding the slogans:
   • a matrix column is a vector;
   • a matrix row is a covector (row vector);
   • vectors and covectors have a dimensionality, parallel to set cardinality (the dedekind.sets:cardinality ladder);
   • a matrix is both a horizontal concatenation of column vectors and a vertical concatenation of row vectors;
   • a matrix therefore carries two dimensionalities: row count and column count;
   • matrices over a ring form at least a submodule, and under full module axioms a module;
   • matrices over a field form at least a ring; invertible matrices additionally carry the inverse operation (loosely, "sometimes a field" — GLₙ(F) is a multiplicative group, and in the 1×1 case the full ring structure collapses to the field F itself);
   • matrix multiplication is associative but not commutative in general, and composes as a linear map;
   • matrices are equipped with all the ring operations plus transpose.

Note

"Nullity is not nothingness; it is the complement of reach." – Anonymous lecture note, Linear Algebra II, 1990s

See also

#297 undergraduate linear algebra (work in progress): span, kernel and image beyond the rank-nullity contract, and change of basis.