File List

Here is a list of all documented files with brief descriptions:

[detail level 123456]

src
main
modules
dedekind
algebra
algebra.cppm	Groups ⊂ Rings ⊂ Modules ⊂ Polynomials
boolean.cppm	Boolean Starter Package: the algebra on the carrier bool and the canonical embedding 𝔹 ↪ 𝕂3
division.cppm	The Euclidean Engine (Division Rings and Domains)
field.cppm	The Rules of Harmony (Groups, Rings, and Fields)
free.cppm	Free-algebra constructions — the textbook companion to HSP
galois.cppm	Galois fields (finite fields)
group.cppm	The Symmetry of Numbers (ℤ, ℚ*)
halfspace_transport.cppm	Transport of halfspaces along the additive group: the ordered-group slice of the point-free relational DSL (image / inverse / argmax and the entireness inference)
initial_ring.cppm	ℤ as a Form — Initial Ring and Grothendieck group of ℕ
kleene.cppm	Kleene starter: the three-valued truth surface 𝕂3 as an algebra on a set (the downstream sibling of the Boolean 𝔹)
magma.cppm	The Magma: base rung of the algebra tower (an algebraic set)
modules.cppm	The Linear Synthesis (Modules and Vector Spaces)
monoid.cppm	The Additive and Multiplicative Monoids (ℕ)
ordered_algebra.cppm	Ordered-algebra markers and concepts: carriers whose order is compatible with their group / ring / field structure (#664, #895)
polynomial.cppm	The monoid algebra R[M]: polynomials as finitely supported nets over the monomials, and the normal form of a rig's, ring's or field's terms
quotient.cppm	HSP structure-preserving operations on algebras — H (quotient, with a relational congruence reading) + P (direct product) + S (subalgebra) carrier-side concepts; their laws and totality are read off the construction in category:total
registration.cppm	Registration helpers for field-shaped carriers
ring.cppm	The Rules of Harmony (The Semiring Synthesis)
tropical.cppm	The tropical semiring Tropical<T> = T ∪ {∞}, a dioid
universal.cppm	The universal-algebra (A, F) meta-pattern: carrier + finitary operations
vectorspace.cppm	Vector-space concepts + concrete witnesses
analysis
analysis.cppm	Kernels, forms, exterior calculus, Hamiltonian flow
dual.cppm	Dual numbers 𝔻 = a + bε with ε² = 0 — forward-mode AD carrier
exterior.cppm	The Wedge Product and Symplectic Geometry
forms.cppm	The Exterior Algebra (Differential Forms)
ftc.cppm	Fundamental Theorem of Calculus bridge hooks
hamilton.cppm	The Principle of Least Action (Hamiltonian Dynamics)
kernels.cppm	Kernel primitives – Gaussian and reproducing kernels
category
action.cppm	The Morphisms of Influence (Actions and Representations)
adjunction.cppm	Adjoint functors (the Free / Forgetful axis)
automaton.cppm	The matcher of a set of words of one length, specialised to it: the minimal automaton of \(\Sigma^* L\), a value computed by one constexpr function at either binding time
cartesian.cppm	Cartesian Closed Category (CCC) Foundations
cartesian_bicategory.cppm	The meet is the right adjoint of the diagonal (Δ⊣∧), reified
category.cppm	Level 0–4: categorical bedrock + ETCS facade
chain.cppm	Dedekind's chain as a range: the unfold of a seed by a coalgebra, the chain of a step guarded by an end, the arrow mapped along it, the bounded chain [lo, hi], and the default chain of a carrier with the NNO's step (the Jlt paper's Figure 2 and Listing 3, #981). The NNO itself, its step and Lambek's destructor Prior, are :nno's; the folds over a chain are :total's concat and :action's fold
comprehension.cppm	Monad comprehensions over a finite chain: the queries of SQL and LINQ, where, select, order_by and take, and the folds that end them
concrete.cppm	Concrete categories: faithful U : 𝒞 → Set, sub-object machinery, lattice operations on χ-classified sets
discrete.cppm	The Discrete Infrastructure (Points as Arrows)
equivalence.cppm	Equivalence relations: reflexive + symmetric + transitive predicates, composing the existing axiom traits in :species with a new symmetry trait
etcs.cppm	Elementary Theory of the Category of Sets (ETCS) facade
f_algebra.cppm	Initial F-algebras and terminal F-coalgebras
factorisation.cppm	(Regular epi, mono) factorisation system theory — the categorical context for the image-as-coequalizer-of-kernel-pair theorem narrated in :image (#718 Slice 1)
filtered.cppm	Filtered categories — categories whose finite diagrams have a cocone
functor.cppm	The Functorial Spine (Structure Preservation)
image.cppm	Image-as-coequalizer-of-kernel-pair: IsImageOf<S, F> on the mono side and IsCoequalizer<Q, F, G> on the quotient side
involution.cppm	Involution — a direction-reversal that is its own inverse — the atomic shape behind the dagger of a \(\dagger\)-category
iso.cppm	The retract / iso-enabling arrow surface: the constructions that turn a factorisation class into a downstream decidability class
kleisli.cppm	The Kleisli Partition (The Extension Systems)
lattice.cppm	Lattice categories — the Form-chain row 4 (#698)
lattice_term.cppm	The assembled lattice-law term reducer: the normal form of a term over a bounded lattice, built from the induced laws in :lattice, as one algebra for cata, its type at compile time and its value at run time
limit.cppm	Universal Limits: boundary objects (Initial and Terminal) and binary products
logic.cppm	The Rules of Thought (Ω)
mereology.cppm	Embryonic Mereology (Part-Whole and Skew Algebraic Core)
monad.cppm	Monads and Comonads (Context as Algebra)
morphism.cppm	The Skeletal Morphism (Structural Cement)
natural.cppm	Natural Transformations (The Slide between Functors)
nno.cppm	The Natural Numbers Object — Lawvere's ETCS Axiom 9 — and the upstream home of Peano recursion / primitive recursion / the Peano successor (categorical idiom + textbook synonyms below)
numeric.cppm	The Numeric Landing (IEEE 754 and Lipschitz Boundaries)
partial.cppm	The Logic of Potentiality (Partial Algebra)
periodic.cppm	Periodic arrows on the counts and the counts they license: an arrow f is periodic with period p when \(f(k + p) = f(k)\), a law declared at a generator and inferred at a composite, so that a count along a chain of any length is (n div p) periods and a remainder (the Jlt paper's tensor exhibit, #1104)
posetal.cppm	Posetal categories — categories derived from partial orders
pullback.cppm	Limits — Equalizers and Fiber Products (Pullbacks)
runs.cppm	Run lists over a finite chain: a subset of \([0, n)\) as the positions where its membership changes, the canonical form of a decidable set on a chain, bounded by its type and on the stack
small.cppm	Small Categories (Enumerated Morphism Sets)
species.cppm	The Reified Machine (The Taxonomic Bricks)
thin.cppm	Thin categories — categories whose hom-sets contain at most one morphism
topoi.cppm	The Internal Logic of the Topos
total.cppm	The Laws of Total Algebra (The Algebraic Hierarchy)
geometry
affine.cppm	Affine spaces — points, vectors, dimension witnesses
euclidean.cppm	The Study of Distance, Metrics, and Curvature
function.cppm	Concept anchoring for function spaces — #537 slice 1
geometry.cppm	Affine ⊂ InnerProduct ⊂ Euclidean ⊂ Hilbert
hilbert.cppm	Hilbert spaces — Cauchy-complete inner-product spaces
inner_product.cppm	Pre-Hilbert (inner-product) spaces over ℝ or ℂ
lattice.cppm	Geometric lattices (ℤ², ℕ², Gaussian integers in ℂ)
linear_map.cppm	Finite-dim linear maps with algebraic witnesses
outer_product.cppm	Concept-side anchoring for the outer / dyadic / rank-1 product space (#535)
tangent.cppm	Tangent-bundle concepts (flat case)
ieee
approx.cppm	Approximation policies for the IEEE effect context
ieee.cppm	Core IEEE fast lane as explicit physical plumbing
linear_algebra
basis.cppm	Free-module / basis / endomorphism-ring trait registry
contracts.cppm	Rank-nullity and matrix-structural compile-time contracts
diagonal.cppm	Intensional diagonal and rank-1 outer-product matrix carriers (#372 slice c + e) at any dimension, including ℵ_0
embeddings.cppm	Canonical regular representations ℂ ↪ M₂, 𝔻 ↪ M₂
linear_algebra.cppm	Backend-agnostic linear operator contracts
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)
matnxn.cppm	The N×N matrix over a semiring — Mat(S), the higher-rank, semiring-generic generalisation of :mat2x2's Matrix2x2V<T>
matrix.cppm	Matrix-shape carriers — generic n×m matrix aggregator
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
vec2.cppm	Level 12.5a₀: 2-tuples — Vec2 / Vec2V (column) and Covec2V (row)
morphologies
archimedean.cppm	Archimedean / ordered-field convergence stubs
cyclic.cppm	Cyclic-morphology carriers and their concept witnesses
morphologies.cppm	Cyclic and Archimedean morphology carriers
numbers
approx.cppm	Compatibility bridge for IEEE approximation policies
boolean.cppm	Formal definition of the Boolean system 𝔹 within the numeric ontology
cardinality.cppm	Re-export of dedekind.sets:cardinality with numbers-level proofs
collatz.cppm	Bounded Collatz reachability — a §4 relational exhibit on ℕ
complex.cppm	Minimal complex wrapper for experimental reintegration
constants.cppm	Reserved for Dedekind-cut realisations of named reals (empty)
cut.cppm	The genuine real: a decidable Dedekind cut on \(\mathbb{Q}\)
ieee.cppm	Bridge from numerical carriers into the upstream IEEE core module
integer.cppm	Minimal number taxonomy concepts for reintegration
lattice.cppm	Integer lattices in ℝ_d and ℝ_dⁿ
mandelbrot.cppm	Core Mandelbrot recurrence helpers over complex carriers
natural.cppm	The Dictionary of Species (The Registry)
numbers.cppm	Level -1 to 8: The Numerical Tower (ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ)
quadratic.cppm	\(\mathbb{Q}(\sqrt D)\) — a genuine, decidable quadratic real field
quaternion.cppm	The Quaternion Division Ring (ℍ)
rational.cppm	ℚ — rationals as numerator/denominator pairs
real.cppm	The real line: ℝ (the coat-hanger — a set-indexed field over the order-complete carrier QuadraticReal<2>) and the machine ambient ℝ_d over the finite doubles 𝕃<double>
real_bridge.cppm	The Birkhoff S leg \(\mathbb{Q}\hookrightarrow\mathbb{R}\): a genuine monic homomorphism into the \(\mathbb{Q}(\sqrt2)\) coat-hanger, with computed witnesses, plus its graph \(\Gamma=\operatorname{graph}(\text{embed})\subseteq\mathbb{Q}\times \mathbb{R}\) reifying the arrow relationally
scalars.cppm	Semirings as the formal algebraic basis for scalar number systems
symbolic.cppm	Symbolic constants ($\sqrt{2}$, …) as Dedekind cuts
optimization
closure.cppm	Single-source graph closure over a semiring, as a fold over its edges
lp.cppm	Linear programming with the optimum as a typed constant
optimization.cppm	Mathematical programming — optimum as a typed constant
order
completeness.cppm	Density and completeness profiles of orders
halfspace.cppm	Compile-time halfspace predicates on ordered carriers
inclusion.cppm	The inclusion (subset) order on subobject lattices, derived from the structural meet and equality (#831)
lattice.cppm	Order-theoretic meet / join / lattice structures
order.cppm	Order relations and compile-time halfspace predicates
poset.cppm	Preorders, partial orders, directed sets, chains
powerset.cppm	The power set \(\mathfrak{P}(S)\) as a filtered universe over a reified subobject domain Sub(C) (#830)
runs.cppm	Run lists: the normal form of the sets of a chain built from intervals, valued in a species
total.cppm	Total-order layer (stronger than :poset)
python
nanobind_jlt.cpp	Nanobind extension module for the Jlt arrow DSL (#961)
nanobind_pst.cpp	Nanobind extension module for Pst: the truth chains (#1001) and the sets over them, per the paper's Lwv grammar (#975)
relational
dyadic.cppm	Tarski's calculus of (dyadic) relations: converse R°, the relative product R;S, union/meet, the diagonal Δ, over Set<pair> — the BASE partition of dedekind.relational
graph.cppm	The graph of a function as a relation: the analytic arrow f and its set of pairs are one object. A graph is a dyadic (binary) relation (functional \(R\subseteq A\times B\) for \(f:A\to B\); an endorelation only when \(A=B\)), so it lives with the relations (dedekind.relational), not in :sets
relational.cppm	dedekind.relational — a first-class module for relations, popped out of :sets: Codd's relational model, Tarski's calculus of relations, and graphs (of arrows, binary relations)
rows.cppm	Relations built at run time as terms: arrows \(A \rightsquigarrow B\) between products of carriers, their objects data (#1037)
tables.cppm	Codd's relational model — the query algebra over typed, intensional Sets and Relations (σ select, π-elided, ⋈ join, ∪, ∖, ∩)
sequences
convergence.cppm	Sequence/series convergence predicates and standard test hooks
curve.cppm	The Curve (Continuum-Indexed Morphism Family)
finite.cppm	Compile-time, array-backed realizations of a sequence and a net — the constexpr siblings of the heap-backed Path
fold.cppm	The left fold (catamorphism) over an enumerable sequence
limits.cppm	The Convergence Morphism (Resolution of the Path)
net.cppm	The Path (The Morphism of Enumeration)
path.cppm	The Path (Morphism of Enumeration): a monad and a comonad
pst.cppm	The Pst fragment's normal form: a decidable set over a finite chain, folded into its run list as the chain is walked
ranges.cppm	The bridge between order's intervals and std::ranges iota views, and the bounded sets built on it
relprod.cppm	The relative product \(R;S\) over a FINITE ℕ-prefix middle: the generalization of :relational's Boolean-middle >> (which enumerates {false,true}) to a bounded ℕ carrier \([0,M)\). The \(\exists\)-over-the-middle is a short-circuiting scan (std::ranges::any_of: it stops at the first witness), and the bound M is carried on the composed type so repeated squaring (R;R, (R;R);(R;R), …) stays bounded — the semantic for-loop of bounded transitive closure (#795)
samples.cppm	Named §3 page-2 sample sequences: is_even and fibonacci
sequences.cppm	Sequences, paths, and (co-)Kleisli triples over directed sets
tail_equivalence.cppm	Tail-equivalence of paths: the congruence of "agreeing eventually", tying the sequence layer to the #718 quotient machinery
sets
boundaries.cppm	The Extremal Identities: Universal (V) and Empty (∅) Sets
cardinality.cppm	Cardinality types and the one-word extensional cardinal carrier
computability.cppm	Decidable membership as a compile-time observable
expressions.cppm	Set-builder DSL — comprehension + Boolean connectives
extensional.cppm	ExtensionalSet — the canonical small-finite extensional carrier, with std::set / std::unordered_set round-trips
heterogeneous.cppm	Set expressions ACROSS carriers: the product \(A \times B\), the sum \(A + B\), and the one widening the library ships, ℕ ↪ ℤ
quantifier.cppm	Bounded first-order quantifiers as set operations: \(\exists\) is non-emptiness of a comprehension, \(\forall\) its \(\neg\exists\neg\) dual
recursion.cppm	Inductive sets: χ, the classifier under definition, inside its own comprehension; the former closes the recursion and admits only a descent
sets.cppm	The Dedekind Set Model: Concrete Collections and Set Morphisms
singleton.cppm	The equality atom: the point {x} as a comprehension over 𝔸<T>
terms.cppm	The term grammar of comprehensions: projections, constants carried as values, arithmetic, arrows applied to terms, conditionals; the comparison atom over two terms; the pointwise connectives of relational predicates
topology
neighborhood.cppm	The Rules of Continuity (Neighborhoods, Limits, and Cuts)
topology.cppm	Open-sets, neighbourhood filters, and continuity witnesses