dedekind.linear_algebra Module Reference

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.
concept	dedekind::linear_algebra::IsLinearOperator
	A linear operator: a (callable) IsArrow that additionally preserves the semimodule structure (the right-S-semimodule-hom law above — sound over any semiring, no commutativity assumed).
concept	dedekind::linear_algebra::IsDimension
	A type-template witness for a dimension cardinality. Today's inhabitants: dim_finite<N> and dedekind::sets::ℵ<N>.

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< O >
	The dual (opposite) orientation — the type-level column↔row flip the transpose / dagger of a 1-tensor performs (a Ket becomes a Bra and vice versa). More...
struct	dedekind::linear_algebra::dual_orientation< ColumnOrientation >
struct	dedekind::linear_algebra::dual_orientation< RowOrientation >
struct	dedekind::linear_algebra::Vec2< T, x, y >
	Structural 2-tuple with coordinates at the type level. More...
struct	dedekind::linear_algebra::Covec2V< T >
	Value-level row vector (covector) of length 2, viewed as a 1×2 matrix. More...
struct	dedekind::linear_algebra::Vec2V< T >
	Value-level column vector of length 2, viewed as a 2×1 matrix. More...
struct	dedekind::linear_algebra::Vec2Map< T, F >
	f on every entry: the vec2_functor's action on an arrow, an endomap of the entries applied entrywise. More...
struct	dedekind::linear_algebra::vec2_functor< T >
struct	dedekind::linear_algebra::Covec2Map< T, F >
	f on every entry: the covec2_functor's action on an arrow, an endomap of the entries applied entrywise. More...
struct	dedekind::linear_algebra::covec2_functor< T >
struct	dedekind::category::unit_witness< dedekind::linear_algebra::vec2_functor< T >, T >
struct	dedekind::category::unit_witness< dedekind::linear_algebra::covec2_functor< T >, T >
struct	dedekind::category::counit_witness< dedekind::linear_algebra::vec2_functor< T >, T >
	Counit / extract witness for Vec2V<T>. Canonical projection to the first coordinate; mirrors the Reader-monad π_0 counit. More...
struct	dedekind::linear_algebra::Invertible2x2< T, a, b, c, d >
	Full-rank 2×2 matrix with entries as non-type template parameters. More...
struct	dedekind::linear_algebra::Matrix2x2< T, a, b, c, d >
	General (possibly-singular) 2×2 matrix with NTTP entries. More...
struct	dedekind::linear_algebra::DirectSum< A, B >
	Direct sum of two invertibles — the trivial compositional preserver. More...
struct	dedekind::linear_algebra::BlockUpperTriangular< A, B, D >
	Block-upper-triangular matrix — Tier 2 of #366, the degenerate-Schur case where the lower-left block is zero. More...
struct	dedekind::linear_algebra::Matrix2x2V< T >
	Value-level 2×2 matrix — the runtime companion to NTTP Matrix2x2. More...
struct	dedekind::linear_algebra::Matrix2x2Map< T, F >
	f on every entry: the matrix2x2_functor's action on an arrow, an endomap of the entries applied entrywise. More...
struct	dedekind::linear_algebra::matrix2x2_functor< T >
struct	dedekind::category::unit_witness< dedekind::linear_algebra::matrix2x2_functor< T >, T >
struct	dedekind::category::counit_witness< dedekind::linear_algebra::matrix2x2_functor< T >, T >
	Counit / extract for Matrix2x2V<T>: top-left corner. Matches the m11 = (1, 1) entry — the canonical projection from the matrix algebra to the underlying scalar ring. More...
struct	dedekind::linear_algebra::SemimoduleVec< S, N, Orientation >
	An N-entry semimodule vector over the semiring S, read as an index→scalar arrow. IsColumnVector / IsCovector by the default (semimodule) contract: ⊕ and the two-sided scalar ⊗ action, but no negation (a dioid has none). Ket (ColumnOrientation, |v⟩) and Bra (RowOrientation, ⟨w|) are its two orientations — the bra·ket language of :transfer made first-class carriers, the "matrix column/row @b is a vector" slogan for a semiring. One carrier, orientation as a template parameter (the tag is the only difference between a column and a row). More...
struct	dedekind::linear_algebra::MatNxNV< S, N >
	Mat(S): the N×N matrix over a semiring S. Entries are stored row-major; ⊕ / ⊗ are S's semiring operations, read off dedekind::algebra::semiring_ops (never native operator+/*, which the tropical carriers skew). More...
struct	dedekind::linear_algebra::TransposeF< S, N >
	The transpose reified as a dagger functor: TransposeF{}(A) = Aᵀ. A value/type (not a free call), so the point-free dedekind::category dagger predicates and concepts (is_unitary, IsDagger, IsUnitary) can take it as their Dagger argument. On Mat(S) the dagger is the transpose; on Rel it is converse; on a Hilbert space the adjoint — :involution unifies the three. More...
struct	dedekind::linear_algebra::dim_finite< N >
	Type-level witness for a finite dimension N. Sibling of dedekind::sets::ℵ<N> on the infinite side; together they cover the dimension axis used by Diagonal / OuterProduct without forcing the std::variant<> Cardinality value to appear as an NTTP. More...
struct	dedekind::linear_algebra::Diagonal< D, F >
	Diagonal matrix carrier M: D×D → T parametric in dimension D and diagonal rule F. More...
struct	dedekind::linear_algebra::identity_rule< T >
	Identity rule: i ↦ T{1}. IsArrow witness for the constant unit. More...
struct	dedekind::linear_algebra::zero_rule< T >
	Zero rule: i ↦ T{0}. More...
struct	dedekind::linear_algebra::one_hot< T, D >
	The one-hot / basis vector e_k : j ↦ δ(j,k) = [j=k] (T{1} on its own index k, T{0} elsewhere) — a 1-arg IsArrow, the k-th COLUMN of the identity Identity (the Kronecker δ with one leg fixed; Diagonal 's entry is δ_ij·F). More...
struct	dedekind::linear_algebra::diagonal_product_rule< F, G >
	The componentwise rule (F·G)(i) = F(i) · G(i). More...
struct	dedekind::linear_algebra::OuterProduct< U, V, Mult >
	Rank-1 matrix M = u⊗v with M[i][j] = u(i)⊗v(j), the product taken in a semiring. More...
struct	dedekind::linear_algebra::Scaled< F, Mult >
	The scalar ⊗-action on an arrow f : D → S: \((c \odot f)(x) = c \otimes f(x)\). An IsArrow (the scaled vector), carrying the scalar c and the arrow f. More...
struct	dedekind::linear_algebra::PointwiseSum< F, G, Add >
	The pointwise ⊕ of two arrows over a shared domain: \((f \boxplus g)(x) = f(x) \oplus g(x)\). An IsArrow (the sum vector). More...
struct	dedekind::linear_algebra::Reflected< F >
	Reflect an arrow through the origin of its domain: \((U f)(x) = f(-x)\) — the parity operator U precomposed onto f. The third intensional combinator (beside Scaled / PointwiseSum) that completes the surface: with them it ASSEMBLES the even projector \(P = \tfrac12(I+U)\) as scaled(½, pointwise_sum(f, reflected(f))), rather than hand-rolling pointwise + and scalar ·. Requires the domain to carry unary negation (found by ADL on the domain type). More...

Typedefs
using	type = RowOrientation
using	type = ColumnOrientation
template<typename O>
using	dedekind::linear_algebra::dual_orientation_t = typename dual_orientation<O>::type
template<typename T = int>
using	dedekind::linear_algebra::Identity2x2 = Invertible2x2<T, T{1}, T{0}, T{0}, T{1}>
	The 2×2 identity matrix over T: [[1, 0], [0, 1]].
template<typename T = int>
using	dedekind::linear_algebra::Zero2x2 = Matrix2x2<T, T{0}, T{0}, T{0}, T{0}>
	The 2×2 zero matrix — the additive identity in the ring of matrices.
template<typename S, std::size_t N>
using	dedekind::linear_algebra::Ket = SemimoduleVec<S, N, ColumnOrientation>
	|v⟩: a column of Mat(S) (a ColumnOrientation vector).
template<typename S, std::size_t N>
using	dedekind::linear_algebra::Bra = SemimoduleVec<S, N, RowOrientation>
	⟨w|: a row of Mat(S) (a RowOrientation covector).
template<typename D, typename T>
using	dedekind::linear_algebra::Identity = Diagonal<D, identity_rule<T>>
	Identity matrix as Diagonal<D, identity_rule<T>>.
template<typename D, typename T>
using	dedekind::linear_algebra::DiagonalZero = Diagonal<D, zero_rule<T>>
	Zero diagonal as Diagonal<D, zero_rule<T>>.
template<typename S, std::size_t N>
using	dedekind::linear_algebra::SquareMatrix = MatNxNV<S, N>
	A dense N×N semiring matrix — the extensional adjacency carrier a relation materialises to. Finite N by construction, hence the IsExtensional witness the star's fixpoint needs. This is Mat(S) (MatNxNV, :matnxn), the certified matrix semiring; the alias keeps the transfer-local spelling while ⊕/⊗ and the *-closure come from semiring_ops<Mat(S)>, not hand-rolled here.

Functions
template<typename T, T a, T b, T c, T d, T a2, T b2, T c2, T d2>
constexpr auto	dedekind::linear_algebra::operator* (Invertible2x2< T, a, b, c, d >, Matrix2x2< T, a2, b2, c2, d2 >)
	Mixed composition: Invertible2x2 · Matrix2x2 → Matrix2x2.
template<typename T> requires std::semiregular<T> && dedekind::algebra::HasRingOperators<T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::inverse (const Matrix2x2V< T > &a, std::plus< Matrix2x2V< T > >)
	The additive inverse, \(-A\) entry by entry: the hook category::inverse_v reads, found by argument-dependent lookup.
template<typename T>
constexpr Vec2V< T >	dedekind::linear_algebra::operator* (const Matrix2x2V< T > &A, const Vec2V< T > &v)
	Matrix-column-vector product: (2×2) · (2×1) → (2×1).
template<typename T>
constexpr Covec2V< T >	dedekind::linear_algebra::operator* (const Covec2V< T > &v, const Matrix2x2V< T > &A)
	Row-vector-matrix product: (1×2) · (2×2) → (1×2).
template<typename T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::operator| (const Vec2V< T > &a, const Vec2V< T > &b)
	Horizontal concatenation of two column vectors into a 2×2 matrix.
template<typename T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::operator/ (const Covec2V< T > &a, const Covec2V< T > &b)
	Vertical concatenation of two row vectors into a 2×2 matrix.
template<typename S, std::size_t N, typename O> requires (IsColumnVector<SemimoduleVec<S, N, O>> || IsCovector<SemimoduleVec<S, N, O>>)
constexpr SemimoduleVec< S, N, dual_orientation_t< O > >	dedekind::linear_algebra::transpose (const SemimoduleVec< S, N, O > &v)
	The dagger of a 1-tensor: transpose flips the orientation (Ket ↔ Bra), keeping the components — so \(\mathrm{dagger}(|v\rangle)=\langle v|\) and \(\mathrm{dagger}(\langle w|)=|w\rangle\) ( \((n\times1)^{\top}=1\times n\)).
template<typename S, std::size_t N>
constexpr MatNxNV< S, N >	dedekind::linear_algebra::zero_matrix ()
	The zero matrix — every entry the base ⊕-identity (0̄).
template<typename S, std::size_t N>
constexpr MatNxNV< S, N >	dedekind::linear_algebra::identity_matrix ()
	The identity matrix — ⊗-identity (1̄) on the diagonal, 0̄ off it.
template<typename T> requires dedekind::numbers::IsComplexScalar<T> && dedekind::algebra::HasRingOperators<T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::as_matrix2x2 (const Complex< T > &z)
	Regular representation of ℂ inside M₂(T): a + b·i ↦ [[a, -b], [b, a]].
template<typename T> requires dedekind::numbers::IsComplexScalar<T> && dedekind::algebra::HasRingOperators<T>
constexpr Complex< T >	dedekind::linear_algebra::complex_from_matrix2x2 (const Matrix2x2V< T > &M)
	Left inverse of as_matrix2x2 on matrices of complex form.
template<typename T> requires std::semiregular<T> && dedekind::algebra::HasRingOperators<T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::as_matrix2x2 (const Dual< T > &d)
	Regular representation of 𝔻 inside M₂(T): a + b·ε ↦ [[a, b], [0, a]].
template<typename T> requires std::semiregular<T> && dedekind::algebra::HasRingOperators<T>
constexpr Dual< T >	dedekind::linear_algebra::dual_from_matrix2x2 (const Matrix2x2V< T > &M)
	Left inverse of as_matrix2x2 on matrices of dual form.
template<typename D, typename F, typename G> requires IsDimension<D> && dedekind::category::IsArrow<F> && dedekind::category::IsArrow<G>
constexpr auto	dedekind::linear_algebra::operator* (Diagonal< D, F > const &a, Diagonal< D, G > const &b)
	Diagonal-times-diagonal: returns the componentwise-product diagonal at the same dimension D.
template<typename F> requires dedekind::category::IsArrow<F> && std::semiregular<typename std::remove_cvref_t<F>::Codomain> && dedekind::algebra::HasRingOperators< typename std::remove_cvref_t<F>::Codomain>
constexpr Matrix2x2V< typename std::remove_cvref_t< F >::Codomain >	dedekind::linear_algebra::to_dense (Diagonal< dim_finite< 2 >, F > const &d)
template<std::size_t N, typename Bra, typename Ket, typename S = typename std::remove_cvref_t<Bra>::Codomain, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsArrow<Bra> && dedekind::category::IsArrow<Ket> && dedekind::category::IsSemiring<S, Add, Mult>
constexpr S	dedekind::linear_algebra::inner_product (const Bra &w, const Ket &v)
	The bra·ket inner product ⟨w|v⟩ = ⊕_{k<N} w(k) ⊗ v(k) over a semiring. Bra w and ket v are IsArrow factors (index → scalar); N is the shared dimension.
template<typename S, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsSemiring<S, Add, Mult>
constexpr S	dedekind::linear_algebra::geometric_sum (const S &r, std::size_t N)
	The structure-directed finite geometric sum \(\sum_{k=0}^{N-1} r^k\), in closed form.
template<typename F, typename S = typename std::remove_cvref_t<F>::Codomain, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsArrow<F> && std::same_as<std::remove_cvref_t<S>, typename std::remove_cvref_t<F>::Codomain> && dedekind::category::IsSemiring<S, Add, Mult>
constexpr Scaled< std::remove_cvref_t< F >, Mult >	dedekind::linear_algebra::scaled (S c, F f)
	Scale an arrow by a scalar — the \(c \odot f\) semimodule action.
template<typename F, typename G, typename S = typename std::remove_cvref_t<F>::Codomain, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsArrow<F> && dedekind::category::IsArrow<G> && std::same_as<typename std::remove_cvref_t<F>::Domain, typename std::remove_cvref_t<G>::Domain> && std::same_as<S, typename std::remove_cvref_t<G>::Codomain> && dedekind::category::IsSemiring<S, Add, Mult>
constexpr PointwiseSum< std::remove_cvref_t< F >, std::remove_cvref_t< G >, Add >	dedekind::linear_algebra::pointwise_sum (F f, G g)
	Add two arrows pointwise — the \(f \boxplus g\) semimodule addition. Both factors must share Domain and Codomain.
template<typename F> requires dedekind::category::IsArrow<F> && requires(const std::remove_cvref_t<F>& cf, const typename std::remove_cvref_t<F>::Domain& x) { cf(-x); }
constexpr Reflected< std::remove_cvref_t< F > >	dedekind::linear_algebra::reflected (F f)
	Reflect an arrow through its domain origin — the parity U.
template<std::size_t N, typename A, typename B, typename S = std::remove_cvref_t<std::invoke_result_t<A, std::size_t, std::size_t>>, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsSemiring<S, Add, Mult>
constexpr S	dedekind::linear_algebra::matmul_entry (const A &a, const B &b, std::size_t i, std::size_t j)
	The semiring matrix-product entry (A⊗B)(i,j) = ⊕_{k<N} A(i,k) ⊗ B(k,j). A and B are any (i,j)→S entry maps (e.g. an OuterProduct); N is the contracted (middle) dimension.
template<std::size_t N, typename U, typename V, typename Mult>
constexpr auto	dedekind::linear_algebra::eigenvalue (const OuterProduct< U, V, Mult > &m)
	The rank-1 eigenvalue of a dyad M = |v⟩⟨w|: λ = ⟨w|v⟩. Over a commutative semiring M² = λ·M — λ is central, so it factors out of M²(i,j) = v_i ⊗ λ ⊗ w_j; the tropical carriers (max-plus / min-plus) are commutative. Over a noncommutative semiring the middle scalar stays put (v_i ⊗ λ ⊗ w_j) and does not collapse to λ·M. Reads the dyad's factors straight off the OuterProduct.
template<std::size_t L, typename Bead, typename S = std::remove_cvref_t<std::invoke_result_t<Bead, std::size_t>>, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsSemiring<S, Add, Mult>
constexpr S	dedekind::linear_algebra::transfer_chain (Bead bead)
	The closure of a length-L chain of transfers: the ⊗-fold of their per-bead eigenvalues ⊗_{m<L} bead(m). A structured fold whose accumulator is a single scalar — because each transfer is rank-1, that scalar is the entire memo (dim = rank = 1). Intensional: bead is an index→λ map, and nothing materialises until the value is forced ("realize it when you mean it").
template<std::size_t N, typename Rel, typename S = rel_codomain_t<Rel>, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsSemiring<S, Add, Mult>
constexpr SquareMatrix< S, N >	dedekind::linear_algebra::ext (const Rel &rel)
	THE JOINT: materialise a binary endorelation on a semiring into its dense extensional adjacency SquareMatrix — the generic (black-box) fiber of the relation→matrix map (§ the paper's classification table). rel is (i,j)→S over the same finite index carrier [0,N) on both sides (hence endo, hence square), with the codomain S an IsSemiring (so ⊕/⊗ and thus star are defined). The compile-time bound N is the extensionality constraint: an infinite relation has no such N and cannot form a matrix, so the Rice wall lives in this signature. Structured relations (functional, bijective, rank-1) admit specialised fibers (sparse, orthogonal, low-rank); this is the base case.
template<std::size_t N, typename S, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsSemiring<S, Add, Mult>
constexpr SquareMatrix< S, N >	dedekind::linear_algebra::star (const SquareMatrix< S, N > &A)
	The Kleene star A* = ⨆ₙ Aⁿ = Δ ⊕ A ⊕ A² ⊕ … — R* as a running corollary of the generic closure, iterating M ↦ Δ ⊕ M⊗A to its fixpoint on the extensional matrix. Over Bool it is reachability; over MaxPlus the longest path (the algebraic path problem). Discharges FIXME(#786) for R* as a matrix corollary; the SquareMatrix argument is the extensionality the intensional relation lacked.
template<std::size_t N, typename S>
constexpr SquareMatrix< S, N >	dedekind::linear_algebra::transpose (const SquareMatrix< S, N > &A)
	The extensional dagger: the transpose Aᵀ (swap i,j) of an already-materialised matrix. The dagger itself is converse (the intensional predicate swap R°(i,j) = R(j,i), see the witnesses); this transpose is only its materialised realisation, worth forming when a physical layout is wanted (cache locality) rather than as the operation. On Rel the dagger is converse, on a real space the transpose, on a Hilbert space the adjoint; it reverses every arrow, so (R°)* = (R*)° is CPM's backward pass (the latest-start times).

Variables
static constexpr std::size_t	ambient_dimension = AmbientDimension
static constexpr std::size_t	rank = Rank
static constexpr std::size_t	nullity = AmbientDimension - Rank
template<typename T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::identity_matrix2x2_v {T{1}, T{0}, T{0}, T{1}}
	Value-level identity: [[1, 0], [0, 1]].
template<typename T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::zero_matrix2x2_v {T{0}, T{0}, T{0}, T{0}}
	Value-level zero: [[0, 0], [0, 0]].
template<typename M, typename R, std::size_t N>
constexpr bool	dedekind::linear_algebra::is_free_module_v = false
	is_free_module_v<M, R, N>: declare that M is a free module of rank N over R.
template<typename A, typename V>
constexpr bool	dedekind::linear_algebra::is_endomorphism_ring_v = false
	is_endomorphism_ring_v<A, V>: declare that A is the endomorphism ring of the module V, i.e.\ A = End_R(V) for the appropriate scalar R.
template<typename F>
constexpr bool	dedekind::linear_algebra::is_linear_operator_v = false
	Opt-in: F is a linear operator — a semimodule homomorphism, additive and scalar-equivariant on the matching side: \(f(x\otimes s \oplus y) = f(x)\otimes s \oplus f(y)\).
template<typename S, std::size_t N>
constexpr bool	dedekind::linear_algebra::is_linear_operator_v< MatNxNV< S, N > > = true
	Mat(S) is a linear operator on \(S^N\) — a semimodule homomorphism over any semiring S (the lower bound; no commutativity required).

Files
file	src/main/modules/dedekind/linear_algebra/linear_algebra.cppm
	Backend-agnostic linear operator contracts.
file	src/main/modules/dedekind/linear_algebra/basis.cppm
	Free-module / basis / endomorphism-ring trait registry.
file	src/main/modules/dedekind/linear_algebra/contracts.cppm
	Rank-nullity and matrix-structural compile-time contracts.
file	src/main/modules/dedekind/linear_algebra/diagonal.cppm
	Intensional diagonal and rank-1 outer-product matrix carriers (#372 slice c + e) at any dimension, including ℵ_0.
file	src/main/modules/dedekind/linear_algebra/embeddings.cppm
	Canonical regular representations ℂ ↪ M₂, 𝔻 ↪ M₂.
file	src/main/modules/dedekind/linear_algebra/mat2x2.cppm
	2×2 matrices — as linear maps between 2-tuples (the worked first-class instance; n>2 lives behind the structure-preserving combinators of #368).
file	src/main/modules/dedekind/linear_algebra/matnxn.cppm
	The N×N matrix over a semiring — Mat(S), the higher-rank, semiring-generic generalisation of :mat2x2's Matrix2x2V<T>.
file	src/main/modules/dedekind/linear_algebra/matrix.cppm
	Matrix-shape carriers — generic n×m matrix aggregator.
file	src/main/modules/dedekind/linear_algebra/transfer.cppm
	Semiring-generic low-rank transfer operators: the bra·ket inner product, the ⊕/⊗ matrix-product kernel, and the rank-1 collapse D² = λ·D that makes a transfer power analytic.
file	src/main/modules/dedekind/linear_algebra/vec2.cppm
	Level 12.5a₀: 2-tuples — Vec2 / Vec2V (column) and Covec2V (row).