Concepts

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

[detail level 1234]

Ndedekind
Nalgebra
RIsDivisionRing	A Ring establishing the existence of Multiplicative Inverses
RIsEuclidean	A Commutative Ring endowed with a division algorithm
RHasFieldOperators	Pure syntactic shape: T closes strictly under the full field operator surface +, binary -, unary -, *, /, and exposes the multiplicative unit T{1}
RIsField	The set-indexed lift of the axiomatic category::IsField: a set object X whose carrier X::Domain is a field
RIsAlgebraicallyClosed	The "Soul" of the Field: Every polynomial has a root in the species
RIsGaloisField	A finite field, as an algebraic set: an ETCS set X whose carrier X::Domain is an axiomatic field with the carrier-author finite-cardinality opt-in
RHasGroupOperatorsAdd	Pure syntactic shape: T closes strictly under the additive-group operator surface +, binary -, unary -
RHasGroupOperatorsMul	Pure syntactic shape: T closes strictly under the multiplicative-group operator surface *, /, and exposes the multiplicative unit T{1}
RHasSuccessorOperators	Pure syntactic shape: T supports the successor / predecessor operator surface (pre- and post-increment / -decrement, all four)
RHasCompoundGroupOperatorsAdd	Pure syntactic shape: T supports the in-place additive-group operator surface +=, -=
RHasCompoundGroupOperatorsMul	Pure syntactic shape: T supports the in-place multiplicative-group operator surface *=, /=
RIsGroup	Proposition: a set object X whose carrier X::Domain forms a group — the set-indexed lift of category::IsGroup
RIsAdditiveGroup	Proposition: a set object X whose carrier is a group under +
RIsMultiplicativeGroup	Proposition: a set object X whose carrier is a group under *
RIsArithmeticAdditiveGroup	The ℤ-deal: a carrier that is an additive group AND whose group structure agrees with the standard C++ +, -, unary - operators
RIsInitialRing	R is the initial object in Ring — for every ring S there exists a unique ring homomorphism R → S
RIsGrothendieckGroup	G is the Grothendieck group of the commutative monoid M — the free abelian group on M, equivalently the left adjoint of the forgetful functor Ab → CMon applied at M
RIsMagma	Proposition: a set object X whose carrier X::Domain forms a magma — the set-indexed lift of category::IsMagma
RIsIntegralScalar	Internal bridge for std::integral scalar carriers
RIsUnsignedIntegralScalar	Internal bridge for std::unsigned_integral scalar carriers
RIsFloatingScalar	Internal bridge for std::floating_point scalar carriers
RIsModule	An Abelian Group participating in a Linear Action by a Ring
RIsScalar	A bona fide scalar is a 1D semi-module over itself
RIsMonoid	Proposition: a set object X whose carrier X::Domain forms a monoid — the set-indexed lift of category::IsMonoid
RIsAdditiveMonoid	Proposition: a set object X whose carrier is a monoid under +
RIsMultiplicativeMonoid	Proposition: a set object X whose carrier is a monoid under *
RIsOrderedAdditiveGroup	An additive group whose order is translation-invariant
RIsOrderedMultiplicativeGroup	An ordered field — the textbook home of multiplicative scaling of halfspaces
RIsOrderedCommutativeRing	A commutative ring whose carrier is ordered under the additive translation marker
RHasRingOperators	Pure syntactic shape: T closes strictly under +, -, * (binary and unary -). Textbook closure — results are exactly T, not just convertible to T
RIsSemiring	The set-indexed lift of category::IsSemiring (an exact alias of category::IsRig): the "rig" rung of the tower
RIsRig
RIsRng
RIsRing	The set-indexed lift: a set object X whose carrier X::Domain is both a Semiring AND an Abelian Group under addition
RIsArithmeticRing	The seal: a carrier that is a ring AND whose ring structure agrees with the standard C++ arithmetic operators
RIsCommutativeRing	A Ring where multiplication is also commutative
RHasSemiringOperators	Pure syntactic shape: T closes strictly under + and *, with structural identities T{} and T{1}
RIsRingHomomorphism	A callable φ from Source to Target that carries the ring structure: \(\varphi(a + b) = \varphi(a) + \varphi(b)\), \(\varphi(a b) = \varphi(a) \varphi(b)\), \(\varphi(0) = 0\) and \(\varphi(1) = 1\) (Lang, Algebra, §II.1)
RIsTropical	A dioid: an IsSemiring whose additive monoid Add is idempotent (a semilattice). This is the algebraic gate for the tropical carriers, refining IsSemiring exactly by ⊕-idempotence
RIsClosedAlgebra	The closure-only tier of an (A, F) algebra: each Op closes on T, without the value-semantics requirement
RIsAlgebra	The universal-algebra (A, F) pattern at the closure tier
RIsAlgebraOnSet	An algebraic set: a Tarski set whose carrier is closed under a family of operations. This is the Ddk = Trsk ∩ Alg layer, spelt out as its two conjuncts
RIsTotalAlgebra	The universal-algebra (A, F) pattern at the totality tier — every operation closes on the carrier and is total under the carrier's chosen totality path (Periodic / Idempotent / Saturating)
RHasCarrier	The HAS-A posture in code: an Algebra HAS-A Carrier (under operations Ops) iff the carrier closes the operations (IsAlgebra), the carrier is mereologically a part of the algebra, and the algebra exposes the part via the arrow_drill_down projector
RAlgebraAsProduct	Set-level sibling of HasCarrier: an algebra is a product of (set object, operations on the underlying type)
RIsHomomorphism	An arrow \(f : A \to B\) between two algebras that carries each operation of the signature S on \(A\) to the one in the same place of T on \(B\): \(f(x \odot y) = f(x) \circledast f(y)\) and \(f(e) = e'\) for each (Burris and Sankappanavar, A Course in Universal Algebra, §II.6)
RIsQuotientMorphism	An arrow that is both a homomorphism of the signatures and surjective (via category::is_epic_arrow_v)
REmbedsAsSubalgebra	The Birkhoff S leg as an arrow: a monic homomorphism, i.e. a structure-preserving embedding whose image is a subalgebra
RIsVectorSpace	The Gold Standard: A Module where the Scalar is a Field
RIsFieldElement	A bona fide element of a field is a 1D vector space over itself
RHasVectorSpaceOperators	Pragmatic vector-space check used by first reified vector carriers
RSatisfiesVectorSpaceAxioms	Operational witness of the core vector-space axiom signatures
RIsSemimodule	A commutative additive monoid participating in a Linear Action: dedekind::category::IsSemimodule, whose laws are the trait is_linear_action_v there
Ncategory
Ndetail_action
RMultipliesInPlace	A carrier whose product stays in it: no integer narrower than int, whose product promotes to a signed int that may overflow
Ndetail_arrows_witness
RHasSections
Ndetail_comprehension
RIsMaybe
RReadsItsElements	A stage that reads a query's elements: an arrow out of the type its present elements have
RIsForeignView	A view of the caller's, not one of the library's walks
RAscendsByPosition
RKeptByTheWalk	The walk's own order already is Order's under Rank: the chain descends by prior, so its elements fall along it, and a monotone rank under descending, or an antitone one under ascending, keeps them in order. order_by is then the identity
RReversedByTheWalk	The walk's order is Order's reversed: order_by is the query re-rooted on the ascending slice, read upwards
RIsBounded
Ndetail_f_algebra
RHasComponentOrders	Op is a product order with component orders to descend into
Ndetail_kleisli
RIsKleisliStep	A step from A and an element into TA, the monad on A
Ndetail_lattice_nodes
RBuildNodes	Two terms whose | and & build nodes: both opted in, on one domain
Ndetail_limit
RHasIndependentComponents	A point whose components are stored independently, every value of one beside every value of the others: a tuple, a pair-like product, or a carrier that says so. Not a fibred product's point, whose components are read off one value
Ndetail_natural
RIsConstantFamily	A family with one component at every object: component(), the arrow its call returns wherever it is called. Commuting with each lifted arrow makes such a family natural; a family whose component depends on the object needs the square at both ends, which no certificate here states
RIsNaturalSquare	The naturality square at an arrow f, \(\alpha \circ F(f) = G(f) \circ \alpha\), for a component Ac of one type at every object (the single-species categories), decided by the arrow algebra and never by comparing the two composites' types, which differ for any component but an identity although the arrows they denote agree:
Ndetail_periodic
RIsPeriodicPredicate	A periodic predicate on the counts
RIsFactorsOf	A list of factors, a count factorised, in the counts N
RIsBoundedList	Bounded by its type: a forward range with a static capacity
RIsBoundedFactorsOf	A list of factors bounded by its type: the factors of a shape
Ndetail_mat2x2
RHasRingEntries	The entries form a ring under the + and × the matrices are computed with: then M₂(T) is a ring (Lang, Algebra, §XIII.1), each law below inherited from it, and not otherwise
RIsFreeAlgebra	F is declared as the free algebra over some base R
RIsQuotientAlgebra	Q is declared as a quotient of some base algebra
RIsCongruenceQuotient	Q is a quotient of a carrier V by a declared congruence R for Op and reduces from V — the relational reading of the H leg
RIsProductAlgebra	Q is declared as a finite direct product of some base algebra
RIsSubalgebra	Subobject S of A is a subalgebra under operation Op when it is closed under Op
RIsSubalgebraOf	S is declared as a subalgebra of some base algebra
RRegisteredViaHelper
RSpeciesTraitsHasIsAssociative
RSpeciesTraitsHasIsCommutative
RSpeciesTraitsHasIsPeriodic
RSpeciesTraitsHasIsInvertible
RSpeciesTraitsHasIsDistributive
RSpeciesTraitsHasIdentity
RIsLeftAction	The shape of a left action (S ⟳ M), \(S \times M \to M\), scalar first, as a module's: its laws are the certificate a concept above it reads (is_linear_action for a semimodule). A left action of a monoid \(M\) is a right action (IsRightAction) of its opposite, Opposite<Op> (:involution), and over a commutative monoid the two coincide
RIsSemimodule	A commutative monoid M on which the semiring S acts linearly
RHasCountingAction	The counts act on (T, Op) in one step, by a law: the semimodule laws or idempotence
RIsRightAction	H is a right action \(M \times S \to M\) of the monoid (S, Op) that acting_monoid<H> names: M is a right S-set (Mac Lane and Moerdijk), an S-act (Kilp, Knauer and Mikhalev, Monoids, Acts and Categories). A left action is a right action of the opposite, Opposite<Op>
RHasAdjunctionShape	Structural shape: F and U have the categorical signature of an adjoint pair F ⊣ U — F : 𝒟 → 𝒞 (left, free) and U : 𝒞 → 𝒟 (right, forgetful)
RIsFreeFunctor	Directional alias: F is the left adjoint of an adjunction F ⊣ U. Names the free direction — F sends an object d : 𝒟 to its free construction F(d) : 𝒞 (the universal recipient under U)
RIsForgetfulFunctor	Directional alias: U is the right adjoint of an adjunction F ⊣ U. Names the forgetful direction — U drops the structure that distinguishes 𝒞 from 𝒟 (e.g., U_Ring→Rig forgets that you can do −)
RIsUnitOfAdjunction	Structural shape: η is the unit of an adjunction F ⊣ U — a natural transformation id_𝒟 ⇒ U ∘ F
RIsCounitOfAdjunction	Structural shape: ε is the counit of an adjunction F ⊣ U — a natural transformation F ∘ U ⇒ id_𝒞. Dual of IsUnitOfAdjunction
RIsAdjunction	A typed unit/counit witness relating a left and right functor
RIsCovariantFunctor	A covariant functor between posetal categories: an order-PRESERVING arrow. This is IsMonotone read categorically (a monotone map is a functor of posets that preserves the direction of composition), the documented covariant pole of functor variance (#908)
RIsContravariantFunctor	A contravariant functor between posetal categories: an order-REVERSING arrow (IsAntiMonotone read categorically). The contravariant pole; inhabited by the negation NegationArrow ¬ and any Compose that mixes one covariant with one contravariant leg
RIsVariantFunctor	A functor between posetal categories with a definite variance: covariant or contravariant. This is the "@c IsFunctor parametrized with @c IsVariant" umbrella whose poles are IsCovariantFunctor and IsContravariantFunctor, and exactly the leg-shape a Galois connection's adjoints must share (matched variance, below)
RIsOrderEmbedding	An order-preserving embedding: a monic, order-preserving arrow of one ordered set into another. Such an embedding is a covariant functor between the two posetal categories, so IsCovariantFunctor is a conjunct — the classification is derived from the two legs (IsEmbeddingFunctor && IsMonotone), not re-declared per carrier (#908)
RIsGaloisConnection	Structural shape: F and G form a Galois connection F ⊣ G in a posetal setting — the simplest adjunction. Both are monotone arrows; F : P → Q and G : Q → P with the source/target carriers crossed (so F's Codomain matches G's Domain and vice versa). The universal-property test, for monotone legs
RIsClosureOperator	Structural shape: C is a closure operator on a poset P — an arrow C : P → P that is idempotent (C(C(x)) = C(x)), monotone (x ≤ y ⇒ C(x) ≤ C(y)), and extensive (x ≤ C(x)) for all x
RIsExponential	Categorical exponential object B^A — generalised structural recogniser of "eval morphism via call expression" (#698 Slice 6)
RIsArrowExponential	An exponential E : A → B that also satisfies the project's morphism vocabulary (IsArrow with matching Domain / Codomain typedefs). #706
RIsCoproduct	Categorification of std::variant<A, B> as the categorical coproduct (A + B)
RIsCartesianClosed	A Category equipped with Terminal Objects, Products, and Exponentials
RIsProductCategory	A category whose Species is a categorical product (std::pair)
RIsBinaryRelation	A type R is a binary relation A × B → bool if it is callable on A and B and yields a boolean
RIsBinaryFunction	A binary relation R ⊆ A × B is a function when it is left-total AND right-unique
RIsDirectedGraph	A homogeneous binary relation R ⊆ V × V on a vertex set V is a directed graph: each ordered pair (u, v) with R(u, v) == true is an edge
RIsUndirectedGraph	A directed graph R is undirected when its relation is symmetric: R(u, v) iff R(v, u)
RIsCongruence	A homogeneous binary relation R on a carrier V is a congruence w.r.t. operation Op when it is an equivalence relation and respects Op
RHasSubscriptOperator	Syntactic check: s[i] compiles for Seq, Idx
RIsEvalArrow	Seq exposes operator[Idx] and the carrier site has declared it as the CCC eval counit (Mac Lane CWM §IV.6)
RIsCopy	: the DIAGONAL notion Δ:A→A×A --- an arrow whose Codomain is the square of its Domain (the comonoid comultiplication / fan-out). Copy is the canonical MODEL; this concept is the matchable "diagonal" handle. Purely structural: it names the crossed A→A×A signature, not that the map is a↦(a,a) (that is Copy's own obligation). Cartesian only: the non-cartesian ⊗ setting needs the carrier generalized past std::pair (#951); a type carrying more than one arrow reading needs the dom/cod contract (#952)
RIsMerge	: the FOLD notion Δ†:A×A→A --- an arrow whose Domain is the square of its Codomain (the comonoid dagger / binary combiner). Merge<A,Meet> is the canonical MODEL; this concept is the matchable handle. Purely structural: it names the A×A→A signature, so a PROJECTION π:A×A→A also satisfies it (the shape cannot tell a fold from a projection, the same honesty gap as glb-vs-lub). Same seams as IsCopy: carrier past std::pair (#951); the multi-reading dom/cod contract (#952)
RIsMeetAsRightAdjoint	The STRUCTURAL shape of "the meet @c ∧ is the right adjoint of the diagonal @c Δ" (Δ⊣∧): the reified theory this slice postulates as a type-check
RIsTensor	: the structural shape of the parallel product ⊗ --- an arrow whose Domain AND Codomain are product objects (the arrow-half of the product bifunctor). Tensor<R,S> is the canonical MODEL; this concept is the matchable handle. Cartesian only: the non-cartesian monoidal ⊗ (LA outer product) needs the carrier generalized past IsProduct (#951); a type with >1 arrow reading needs the dom/cod contract (#952)
RIsIntegerChain	A chain with integer arithmetic: a discrete total order, locally finite (every bounded interval is finite), so a distributive lattice under min and max, with the NNO's step and the arithmetic operators as a shape. Finite on a machine word, unbounded for a bignum. Not a ring: int's overflow is undefined and a cardinal may saturate at \(\aleph_0\); the ring is IsRing's to claim
RIsCountWord	A word of the counts: an integer chain whose arithmetic wraps at its cyclic order, the unsigned integers but bool, and none narrower than int, whose products promote to a signed int that may overflow. std::size_t is the default throughout
RIsFiniteChainSequence	A sequence on finite chains: an arrow out of the counts, read along a chain of them (the Jlt paper's Figure 2, its vertical arrows). The chain is finite by its descent and ordered by its step, so the sequence needs no set concept; its laws, a period or an order kept or reversed, are laws of the composite chain >> f, and the folds read them (#1133)
RIsQuery	A query: a range whose elements are Maybe, each present or a hole
RIsPrefixKernel	A kernel on the non-empty prefixes of a text: an arrow out of them, a coKleisli arrow of the history comonad, whose answer at a position may read all that came before it and nothing after
RSetAsProduct	Set := (Underlying, Classifier) read as a product, in the projection-access sense
RIsConcrete	A small category C is concrete when its objects are themselves sets — equivalently, when there is a faithful functor U : C → Set
RHasTernarySupport	True when a set object's classifier returns ternary truth values
RIsCompatibleSetPair	Two set objects over the same ambient species and same Ω codomain
RIsDiscreteCategory
RIsSymmetric	Formal verification: Rel(a, b) ⇔ Rel(b, a)
RIsEquality	Rel on T is equality of values (the diagonal)
RIsChainDecidedSymmetric	Symmetry, stated once for every relation on a walkable chain
RIsEquivalence	A binary relation on T that is reflexive, symmetric, and transitive — the textbook equivalence-relation axioms
RIsHashFunction	A callable h on T whose codomain is std::size_t — i.e. an arrow T → size_t
RHasAxiom1Composition	ETCS axiom 1 witness: composition is available for ambient arrows
RHasAxiom2Identity	ETCS axiom 2 witness: identity arrow acts neutrally on A
RHasAxiom3TerminalObject	ETCS axiom 3 witness: terminal object 1 is present
RHasAxiom4WellPointedness	ETCS axiom 4 witness: membership is evaluation through the carrier-as-characteristic-morphism. Post-#681 structural refactor: IsSubobject already requires the structural call shape { s(a) } -> IsΩ, so the membership-as-evaluation reading lands on the IsSubobject witness itself
RHasAxiom5CartesianProduct	ETCS axiom 5 witness: products exist for ambient species A
RHasAxiom6Exponentiation	ETCS axiom 6 witness: exponentials B^A exist (here A^A witness). Uses the named IsArrowExponential refinement (#706) rather than the ad hoc IsExponential && IsArrow combination that lived here previously
RHasAxiom7SubobjectClassifier	ETCS axiom 7 witness: every set is represented by a subobject
RHasAxiom7ClassifierNaturalityWitness	Optional naturality witness for Axiom 7 classifier behavior
RHasAxiom8EmptySet	ETCS axiom 8 witness: initial object 0 is present
RHasAxiom9NNO	ETCS axiom 9 witness: arithmetic species atlas exposes ℕ witness
RIsSplitEpicPair	Structural witness of a split epimorphism e with section s
RHasAxiom10ChoiceSplitEpicWitness	Axiom 10 (choice) support via an explicit split-epi witness shape
RHasAxiom10ChoiceSplitEpicLawSurface	Axiom 10 semantic-law surface (split-epi shape + equality codomain)
RHasAxiom7PullbackReindexingDefinitionalSurface	Axiom 7 definitional reindexing witness surface
RHasAxiom10PowerObjectLattice	ETCS axiom 10 witness: power-object lattice completeness
RHasETCSAxioms	Diaconescu's classical direction (#698 Slice 9 review)
RIsSet	ETCS set: a carrier satisfying the 10 ETCS axioms AND admitting the canonical Set-CCC witness over its ambient species
RIsInitialFAlgebra	Carrier A is the initial F-algebra for endofunctor F with structure map α
RIsTerminalFCoalgebra	Carrier A is the terminal F-coalgebra for endofunctor F with structure map α
RIsTermNode	A node of the term functor: a type that exposes its legs
RSteers	An algebra that steers the fold at T (Mendler style): it recurses into the legs it chooses by cata itself, instead of the strict fold
RIsRegularEpi	An arrow E is a regular epi when it is an epi and registered as the coequalizer of some parallel pair
RIsRegularMono	Dual of IsRegularEpi: an arrow M is a regular mono when it is a mono and the equalizer of some parallel pair
RIsFactorisationSystem	Category C admits the canonical (regular epi, mono) factorisation system. Form-chain row 6 (#718)
RIsRegularCategory	Category C satisfies the regular-category axioms. Pinned for Set and (transitively) every topos
RIsExactCategory	Category C satisfies the exact-category axioms. Sollbruchstelle landing site
RIsDirected	Formal verification of the directedness axiom: ∀ a, b ∈ T. ∃ c ∈ T. Rel(a, c) ∧ Rel(b, c)
RIsCodirected	Formal verification of the codirectedness axiom: ∀ a, b ∈ T. ∃ c ∈ T. Rel(c, a) ∧ Rel(c, b)
RIsFilteredCategory	A thin category whose every finite subset of objects has an upper bound (directedness)
RIsFunctor	The textbook functor (#633): an IsArrow whose Domain and Codomain are (small) categories — a 1-morphism in Cat, Mac Lane §I.3 — carrying a morphism map
RIsShapedFunctor	A 1-morphism mapping CatS -> CatT, refined with the container shape: an IsFunctor that additionally exposes a type-level object map Shape and the action on arrows, F(f)
RIsIdentityFunctor
RIsEndofunctor	A structure-preserving mapping from a Category back to itself (F : 𝒞 → 𝒞)
RIsIterativeEndomorphism	A stabilizing step function on a carrier species
RIsFAlgebra	A carrier A equipped with a structure map F<A> -> A
RIsFCoalgebra	A carrier A equipped with a structure map A -> F<A>
RIsEmbeddingFunctor	A functor that is fully faithful + injective on objects (Mac Lane CWM §IV.4 strong reading; the Yoneda-embedding flavour)
RIsQuotientFunctor	A functor that is a regular epi / coequalizer presentation (Borceux Handbook §4.3)
RIsImageOf	S realises the image of arrow F as a Subobject of Cod<F> — the mono side of the (regular epi, mono) factorisation system pinned in :factorisation
RIsCoequalizer	The categorical dual of IsEqualizer — a Quotient of Cod<F> equating two parallel arrows F, G
RWitnessesFirstIso	Connector witnesses the First Isomorphism Theorem at homomorphism F
RIsInvolution	Stated in arrow language: F is an endomorphism on the object T (IsEndomorphism, domain and codomain T — applying it twice returns to the domain) carrying the certificate \(f \circ f = \mathrm{id}_T\). T defaults to the arrow's domain; a bare callable names it. The object may be presented by many types (morphism__Objects_And_Their_Presentations), so the complement on \(\mathrm{Sub}(T)\) is an involution here, through this one concept
RIsAntiHomomorphism	A map on T that reverses Op, \(f(a \cdot b) = f(b) \cdot f(a)\): a homomorphism into the opposite, Opposite<Op>, read off the homomorphism certificate rather than declared apart
RIsDagger	The \(\dagger\)-category surface built on IsInvolution: IsDagger, the named intermediate IsIsometry, and IsUnitary — where "the converse is the inverse" (bijective relation) and "the transpose is the inverse" (orthogonal matrix) are one theorem
RIsIsometry	A singleton morphism-carrier F (its default value is the arrow) whose dagger is a left inverse: the named non-linear intermediate (Heunen & Vicary). For a value-level carrier, use the is_isometry predicate instead
RIsUnitary	A singleton morphism-carrier whose dagger is its inverse (isometry and coisometry) — a dagger-iso, \(f^\dagger = f^{-1}\). Hence an IsIsomorphism once lifted into the arrow surface (follow-up)
RIsRetractableArrow	A monic arrow that ships with a structurally-known retract, a partial inverse retract(f) : Cod<F> → Maybe<Dom<F>>, discoverable via ADL on F
RIsKleisliTriple	A Kleisli triple ⟨T, η, (−)*⟩ (Manes), the monad in its extension form: the unit and bind, their laws certified by is_kleisli_triple
RIsCoKleisliTriple	A co-Kleisli triple ⟨W, ε, (−)†⟩, the comonad in its extension form: the counit and extend, their laws certified by is_cokleisli_triple
RIsFrobenius	A Frobenius monad (Street): a Kleisli and a co-Kleisli triple on one functor whose μ and δ satisfy the Frobenius law, certified by is_frobenius_monad
RHasKleisliBindOperators	A monadic carrier MA supports Kleisli bind, >>=, with a Kleisli arrow F; >> composes arrows and nothing else
RHasComonadicExtendOperators	A comonadic carrier WA supports comonadic extend, <<=, with a co-Kleisli arrow F
RHasArrowDereferenceOperator	Syntactic check: m.operator->() compiles for M
RIsKleisliDeref	M exposes operator-> and the carrier site has declared it as Kleisli dereference / comonadic extract (Mac Lane CWM §VI; Wadler 1992)
RIsKleisliArrow	An arrow declared to live in the Kleisli category indexed by the monad tag M (constrained by IsDefaultMonadTag)
RIsLatticeCategory	A posetal category that is both filtered and cofiltered, with joins and meets given by the algebraic lattice operations
RIsBoundedLatticeCategory	A lattice category that has a designated bottom (initial) and top (terminal) element — row 5 of the lattice Form-chain (#698 Slice 4)
RHasLogicSpecies	The equational laws a lattice concept induces, as compile-time term-reduction rules over the term AST below. Each law is a decomposable, independently-testable part; the assembled reducer (:lattice_term) applies exactly the laws the supplied carrier proves. The richer the carrier's structure (a bounded chain is the sweet spot; bool the optimal witness), the more laws fire and the further a term collapses
RIsSpeciesTaggedArrow	An arrow that names its logic species and answers in it: Cod
RSameCarrier	Do both operands live in the same, known carrier? The boundary laws require this so a bound of one carrier (e.g. an int ⊤) is never applied as the unit / annihilator of a term whose other operand lives in a different carrier: a mixed-carrier term (⊤ᵢₙₜ ∧ bool-leaf) fails closed. Because the carrier is read via carrier_of, the laws still apply to an arbitrary same-carrier composite subterm (⊤∧X=X even when X is an un-collapsed Meet / Join), not only to leaves. (The glb/lub law forces a shared carrier through OrderComparable; this is its boundary-law counterpart.)
RIsIdempotentLeaf	T's values are determined by its type, so a type-only lattice law (X∧X=X idempotence, a∧¬a=⊥ complement) collapses soundly on it: two same-type instances are necessarily the same value. A runtime-stateful leaf (say a Singleton holding a value, or a predicate with an expected field) is not idempotent, so those laws must not fire on it, else Meet{S{7},¬S{3}} would wrongly collapse to ⊥. This is the value-safety gate the type-level reducer shares with the value-first :lattice_term reducer (#922). Recursive over Meet / Join / Not through idempotent_leaf_v
ROrderComparable	Can A and B be compared in the injected order Ord, at compile time? Both must expose ::value of one carrier type T that is IsPosetal under Ord's resolved relation, and that relation must be default-constructible and constexpr-callable on those values. A registered-but-runtime-only or stateful order therefore fails this guard and the glb/lub collapse stays inactive (fail-closed) rather than hard-erroring
RIsInvolutiveEndofunctor	Involutive endofunctor concept — an endomap F : T → T with F² ≅ Id
RIsHeytingLatticeCategory	A bounded lattice category whose lattice exponentials are witnessed by :cartesian::IsExponential — row 6 of the lattice Form-chain (#698 Slice 6)
RIsBooleanLatticeCategory	A Heyting lattice category whose complement is an involutive endofunctor satisfying the Boolean complement laws — row 7 of the lattice Form-chain (#698 Slice 7)
RIsSubobjectFamilyMember	Compile-time meeting-point pins (#698 Slice 10) — three structurally distinct carriers at the same Form-chain rows
RIsSubobjectLattice	A type S is the carrier of a subobject lattice over S::Domain, with lattice structure induced pointwise from the classifier S::logic_species::Ω
RIsBooleanSubobjectLattice	The Form-chain ≤ relation on a subobject lattice is derivable from meet:
RIsLatticeLess	The injected total order: a caller-supplied comparator with a static consteval less<X,Y>() returning a logic value in its lattice_less_logic (default Boole, i.e. bool). The reported logic must be a full IsOckhamAlgebra, so ::True (accessed by lattice_definitely_less) is guaranteed present. The reducer canonicalises only on a definitely-True result, so an Unknown (undecidable) comparison leaves the operands in authoring order. Total-ness is the caller's obligation (Jlt: asserted downstream), not checked here
RFires	Whether a law fired: its result is not law_inactive
RCombinesMeet	The lattice-law reducer as the algebra of cata (:f_algebra, the one fold). A leaf reduces to itself. A Meet / Join assembles the induced laws over its two reduced operand values, most-collapsing first (bounded ▸ idempotent ▸ complement ▸ absorption ▸ distributivity ▸ glb/lub ▸ the injected leaf-combine), a law returning law_inactive ceding to the next; a rewrite (distributivity, the leaf-combine, De Morgan) is folded again. Less canonicalises the commutative residue. Every decision a law makes on the operand types is made inside decltype as well, so the normal form's type is reduce_t below and its value is this fold at run time: one law, two binding times
RCombinesJoin
RIsMorphicTotal	A Morphism whose Codomain is the Terminal Object (One)
RIsTerminalMorphism	A morphism that maps into the Terminal Object (One)
RIsTerminalObject	A type that plays the role of a terminal object — either the canonical global One (std::monostate, the unique terminal of the ambient category of sets) or an opt-in structural witness via the is_terminal_object_tag typedef
RIsBoundaryProjection	Projection witness from an owning/wrapper whole to a boundary object
RIsProjectedTerminalObject	Terminal-object witness through an optional projection policy
RHasUniqueMorphismTo	Asserts that there exists a unique morphism from T to U = One
RHasUniqueMorphismFrom	Asserts that there exists a unique (unreachable) morphism from Z = Zero to T
RIsInitialObject	A type that plays the role of an initial object — either the canonical global Zero (std::nullptr_t, the unique initial of the ambient category of sets) or an opt-in structural witness via the is_initial_object_tag typedef
RIsBoundaryObject	A type at a lattice / category bound: an initial object (⊥) or a terminal object (⊤)
RIsProjectedInitialObject	Initial-object witness through an optional projection policy
RTupleLike
RIsPairProjection	Whether F is the projection \(\pi_K\) out of a pair: the recogniser the law readers (:cartesian, a product's defining form) and the hyperdoctrine (relational:graph) read. A genuine std::pair only: a pair-like carrier with more state is no product of its two members
RIsProduct	Categorification of std::pair<A, B> as the categorical product (A × B)
RIsArrowProduct	An IsProduct whose projections are genuine MORPHISMS (arrows), not merely the structural callables IsProduct checks
RIsProductProjection	Functional-part projection witness from a product whole to one part
RIsProjectedProduct	Product witness through an optional whole-projection policy
RIsArrowFromProduct	Matches an Arrow whose Domain is a categorical Product (std::pair)
RIsProductParthood	Bridge: a product P with parts A and B IS a mereological parthood in the projection-access reading
RIsCartesian	A small category equipped with a terminal object 1 and binary products × — a "cartesian category" in the textbook sense (Pierce, Basic Category Theory for Computer Scientists §1.4; Awodey)
RIsOckhamAlgebra	The IsOckhamAlgebra Concept (The Algebraic Signature of Truth)
RHasLogicalOperators	Pure syntactic shape: T supports the logical operators &&, ||, ! with closed results
RIsΩ	A truth-object: a type that can serve as the classifier Ω for a logical species
RIsPst	A truth-object that is a bounded chain: an IsΩ classifier whose values are totally ordered
RLogicalMap	A callable Pred that maps T -> Ω for some IsΩ Ω. Captures the notion of a predicate valued in an arbitrary logic species
RIsClassifierAnswer	T is a classifier answer: it names its species
RLiftsTo
RHaveLogicJoin
RLiftableInto	T can be lifted into To's answers: it already is one, or it is a classifier answer whose species' registered embedding into To accepts it and lands in To::Ω (a Truth<L> wrapper is not an L::Ω and is refused)
RIsDeMorganAlgebra	The committed algebraic tower for the truth objects (#901)
RIsBoundedDeMorganChain	A De Morgan algebra whose truth carrier Ω is totally ordered; by the chain-normality theorem this is automatically a Kleene lattice
RIsBooleanLogic	A bounded De Morgan chain whose reflection is a genuine complement (a∧¬a=⊥, a∨¬a=⊤); on a chain this forces the 2-element case 𝔹
RIsTruthObject	Ω may carry a relation's answer in the laws below: it has a top ⊤, the value a law asserts (reflexivity is rel(a, a) = ⊤). bool (top true) is the default; Ternary names its Ω::True, a value type with a species (Percentage, the bounded chains) finds it on the species. A statement of intent, not a certificate: the laws come before logic, so the truth objects are only certified downstream (:logic, IsΩ)
RIsReflexive	Formal verification of the identity relation
RIsTransitive	Formal verification: (a ≤ b ∧ b ≤ c) ⇒ a ≤ c
RIsAntisymmetric	Formal verification: (a ≤ b ∧ b ≤ a) ⇒ a = b
RIsConnex	Formal verification: a ≤ b ∨ b ≤ a
RSupInfOperand	A carrier on which Sup / Inf (and max / min) are a genuine, usable value op: totally ordered (for <) and copy-constructible (the winner is returned by value). This is the CALL gate: Sup{}(1.0, 2.0) is a valid call that returns a value, so raw floats are not excluded here; only the lattice laws fail on them (see SupInfLattice)
RSupInfLattice	A carrier on which max / min (and Sup / Inf) are honest lattice ops: usable (SupInfOperand) and carrying a certified order
RIsWalkableChain	Rel is a stateless relation on a discrete bounded chain T on which a law of Arity variables can be decided: a step (successor, by argument-dependent lookup, as for HasNNOStep), a least and a greatest value (the identities of Sup and Inf), the top reached from the bottom within chain_walk_budget, and nᴬʳⁱᵗʸ within law_evaluation_budget, all as constant expressions (what cannot be evaluated at compile time is simply not decided here, rather than an error)
RIsChainDecidedReflexive	Each law, stated once for every relation on a walkable chain: the certificate the concept reads is the law over the whole chain, for ≤, ≥, ==, or any stateless relation, decided and never registered per operator. A carrier that answers through its own member keeps that answer; a law the compiler cannot evaluate is not decided here. Exported conditions, so a rule elsewhere can yield to these
RIsChainDecidedAntisymmetric
RIsChainDecidedConnex
RIsChainDecidedTransitive
RIsPartRelation	Verifies that a binary operator satisfies Leśniewski's mereological axioms
RIsPartialOrder	Named stage for the partial-order maturity level of parthood
RIsTotalOrder	Linear/total refinement of IsPartialOrder
RIsPartOfRelation	Minimal core part-whole relation yielding Omega
RIsMereologicalJoinMagma	Stage 0 for join-like algebra: closure only
RIsMereologicalMeetMagma	Stage 0 for meet-like algebra: closure only
RIsMereologicalJoinSemigroup	Stage 1 for join-like algebra: magma + associativity
RIsMereologicalMeetSemigroup	Stage 1 for meet-like algebra: magma + associativity
RIsMereologicalMeetBand	Non-commutative meet-like operation (associative + idempotent)
RIsMereologicalJoinBand	Non-commutative join-like operation (associative + idempotent)
RIsAbsorptive	Mutual absorption and internal idempotency for a pair of operations
RIsMereologicalSkewLattice	Non-commutative lattice-style operations (skew lattice fragment)
RIsMereologicalLatticeOperations	Compatibility lattice alias over the skew core + absorption
RIsMereologicalDistributiveLatticeOperations	Mature distributive stage: lattice operations with mutual distribution
RHasExtrema	Structural requirement for Dedekind completeness witnesses
RIsMereologicalCutCandidate	Transitional bridge contract for the soft-to-hard structural cut
RParthood	Skeletal part-whole contract at the concept level
RIsMonad
RIsComonad	The Unified Comonadic Proof: Co-Kleisli Action as Contextual Being
RPresents	S presents the object C: a value convertible to C (the default: the object is one value type), or a type the object names (C::presents)
RIsArrow	A type that knows its own Domain (A) and Codomain (B), objects it maps between: called at the domain's representative, its result presents the codomain (morphism__Objects_And_Their_Presentations)
RIsSmallCategoryShape	The structural prefix of IsSmallCategory (:small): a type naming an ::Arrow, a ::Species and an ::Id, the shape of a category, without its behavioural axioms (id_c, composition closure). IsSmallCategory itself cannot be named here, since :small imports :morphism. It tells a category apart from an object that merely exposes Domain / Codomain aliases: a Path<T>, a sequence \(\mathbb{N} \to T\), is an arrow and an object of Set, not a category (#525)
RIsEndomorphism	Proposition: A Morphism where Domain ≡ Codomain (f: A -> A)
RIsIdentityArrow
RIsIsomorphism	An Arrow f: A -> B with a guaranteed Inverse g: B -> A
RIsConstantArrow	An arrow known to be constant: every argument to one value
RIsMonicArrow	An arrow declared to be a monomorphism (ι: A ↣ B)
RIsEpicArrow	An arrow declared to be an epimorphism (π: A ↠ B)
RIsMagmaHomomorphism	A map on T declared to carry Op to Op2: \(f(a \odot b) = f(a) \circledast f(b)\)
RPreservesUnit	A map on T carries the unit of Op to the unit of Op2, \(f(e) = e'\), computed at the one unit: the comparison is a template argument, so a map that is no constexpr function object is refused rather than an error. The unit half of a monoid homomorphism, and of a homomorphism of any signature whose operations have units
RIsBijectiveArrow	An arrow declared to be both a monomorphism (ι: A ↣ B) and an epimorphism (π: A ↠ B), i.e. an isomorphism of sets (A ≅ B)
RIsInjective	Set-theoretic synonym for IsMonicArrow — an arrow is injective iff distinct inputs yield distinct outputs (f(x) == f(y) → x == y)
RIsSurjective	Set-theoretic synonym for IsEpicArrow — an arrow is surjective iff every codomain element has a preimage (∀ b ∈ B ∃ a ∈ A. f(a) == b)
RIsBijective	Set-theoretic synonym for IsBijectiveArrow — an arrow is bijective iff it is both injective and surjective, i.e. a set-theoretic isomorphism A ≅ B
RHasArrowComposeOperators	Two arrow types F, G compose via >>
RIsDefaultMonadTag
RIsPreTransformation	The raw family of components
RIsTwoMorphism	The bridge between two specific Functors
RIsNaturalTransformation	A family of components, one per object, whose square commutes at every arrow of the source: \(\alpha_Y \circ F(f) = G(f) \circ \alpha_X\) for each \(f : X \to Y\), read at an arbitrary arrow of the source category's one arrow type, not only at its identities, where every family passes
RIsNNO	Structural shape: (N, Z, S) is a Natural Numbers Object — Z is the zero element 1 → N, S is the successor map N → N
RHasNNOStep	A carrier with both NNO steps available: the shape a value-determined point collapse needs (succ(lo) == pred(hi))
RIsNumericSpecies
RIsLipschitzBoundaryPolicy	User-provided Lipschitz boundary policy over a numeric species
RIsNumericHoleClassifier	A characteristic morphism χ: T -> Ω_K3 for numeric support
RIsPotential	Structural isomorphism for "Maybe-like" species
RIsPartialMagma	A textbook-aligned partial binary algebra
RIsPartialAssociative	The Kleene Associativity Law
RHasPartialIdentity	Existence of a Neutral Element in a Partial Universe
RIsPartialSupportClassifier	Characteristic morphism χ: T -> Ω_K3 for partial support
RIsPartialSemigroup
RIsPartialMonoid
RIsPartialLoop	A Partial Monoid with local invertibility on support
RIsPartialCommutativeSemigroup
RIsPartialGroup
RIsPartialAbelianGroup
RHasPeriod	A sequence on finite chains with a declared period, read by period(f): \(f(k + p) = f(k)\) for every k. Periodicity is a sequence's, an arrow out of the counts, not an arrow's in general
RHasUnitPeriod	A sequence constant on its extent by its type: a constant arrow out of the counts, a sequence after one, and the cylinder's factors along the offsets (R2)
RHasCycleType	A permutation of positions with a known cycle type
RHasFactors	A tensor whose count is a product of factors, as many as its type bounds: a shape, so an outer product of two is one too
RIsPosetal	A Category where morphisms are governed by a specific Logic Species (Ω)
RIsTotallyOrderedPosetal	Posetal refinement where the underlying order is total/linear
RIsOrderMeetSemilattice	Order-theoretic meet-semilattice as a commutative refinement
RIsCertifiedOrderMeetSemilattice	Trait-certified meet-semilattice (associative + idempotent + commutative)
RIsOrderJoinSemilattice	Order-theoretic join-semilattice as a commutative refinement
RIsCertifiedOrderJoinSemilattice	Trait-certified join-semilattice (associative + idempotent + commutative)
RIsOrderLatticeOperations	Order-theoretic lattice operations as commutative + absorptive refinement over upstream mereological lattice operations
RIsCertifiedOrderLatticeOperations	Trait-certified lattice operations (commutative semilattices + absorption)
RIsOrderDistributiveLatticeOperations	Distributive lattice refinement over IsOrderLatticeOperations
RIsCertifiedOrderDistributiveLatticeOperations	Trait-certified distributive lattice refinement
RIsPathProjection	Projection contract used by check_path to map objects into an orderable relation carrier
RIsMonotone	An arrow F declared to be order-preserving with respect to the ambient order relation Op
RIsAntiMonotone	An arrow F declared to be order-reversing with respect to the ambient order relation Op
RIsVariant	An arrow with a definite variance: order-preserving (IsMonotone) or order-reversing (IsAntiMonotone). The leg-shape of a Galois connection, whose adjoints are always one or the other. Mirrors :limit::IsBoundaryObject's "X @c || @c dual" disjunction shape
RIsOrderIsomorphism	An arrow that is both an order-preserving map and a bijection
RIsOrderAntiIsomorphism	An arrow that is both an order-reversing map and a bijection
RHasDomain	A type that names its domain: Dom<F> is formed. The guard under which IsInvolution<F> may be asked at all
RIsPullback	The apex of a pullback square over the cospan f: X ⟶ Z, g: Y ⟶ Z: a subobject carrying the two projection legs π₁ ⟶ X, π₂ ⟶ Y
RIsEqualizer	The kernel of a parallel pair (f, g: A ⟶ B)
RIsKernelPair	The pullback of an arrow F against itself — the equivalence relation "have the same F-image" on Dom<F>
RIsPushout	The categorical dual of IsPullback: the apex of a pushout square over the span f: Z ⟶ X, g: Z ⟶ Y, carrying the two coprojection colegs ι1: X ⟶ P, ι2: Y ⟶ P
RIsParallelPair	F and G are a parallel pair of arrows — shared Dom and shared Cod
RIsLocallySmallCategory	Value-level locally-small witness: the Hom-collection of Cat is a set in the metatheory
RIsSmallCategory	A point-free, morphism-only reification of a Category
RIsSpecies	Formal verification that a type has been registered in the Atlas
RHasTotalProduct	Whether T's product is defined on all of T: a word narrower than int multiplies after promotion to int, and the largest product must fit it. unsigned char's does (255 · 255); unsigned short's does not (65535 · 65535 overflows int, undefined as -INT_MIN is), so it is refused as int is. Decided by the compiler: undefined behaviour is no constant expression. Unsigned words only: there the product grows with its factors, so the largest is the one that may overflow, and numeric_limits names it (a type without limits has max() == T{}, and the probe would check only 0 · 0)
RIsTransfinite
RIsFinite
RIsAssociative
RIsCommutative
RIsDistributive	The "Glue" of the Ring: a * (b + c) = a*b + a*c
RIsIdempotent
RIsThinCategory	A category in which every hom-set has at most one morphism
RIsClassifierConstant
RIsPredicate	The Predicate Morphism: the DSL's membership test, i.e. the characteristic arrow \(\chi_A : A \to \Omega\)
RIsCharacteristic	Categorical alias for a Predicate mapping to Ω: the characteristic arrow \(\chi_A : A \to \Omega\) that classifies a subobject (a set)
RIsDecidableCharacteristic	The Boolean refinement of IsCharacteristic: a membership test valued in the dominance Σ, i.e. \(\chi_A : A \to \Sigma\) with \(\Sigma = \Omega\)-decided \(= @c bool\)
RIsDominanceInclusion	The Rosolini inclusion arrow \(\iota : \Sigma \hookrightarrow \Omega\): a map between truth-objects out of the decided fragment
RIsSieve	Signature-level witness for a sieve of arrows into an object
RIsGrothendieckTopology	Signature-level witness for Grothendieck coverage rules over sieves
RIsBundleProjection	A projection morphism π : E -> B for a bundle candidate
RIsFiberBundle	Signature-level witness for a fiber bundle over a base species
RIsSubobject	The categorical witness of a monomorphism ι: S ↣ A — a characteristic morphism χ: A → Ω together with its inclusion
RIsLSet	An L-set: a subobject of a carrier with \(\chi : X \to L\) into a named bounded chain \(L\) (Codomain = L::Ω). The carrier is asked for copies (std::semiregular), not for a decidable ==: the equality of sets is the Rice cycle (#970), not a trait of the carrier, so the relations of a hom-set are a carrier too (𝔸<RelExpr>, #1045). An ETCS set asks decidable equality itself (IsSet, whose classifier construction needs it), as IsArrow asks an archetype of its domain rather than a value type (archetype_t). Pst is asked of the species (an Ockham algebra whose Ω is totally ordered), not of the bare Ω, so a Chain<int> set (Ω = int) qualifies while a bare int never does. The chain is the registered total order (IsTotalOrder: reflexive, transitive, antisymmetric, comparable), not the syntactic std::totally_ordered, so an Ω without certified order laws (a raw float, whose NaN breaks reflexivity) is refused honestly
RIsFiniteChain	A carrier that is a finite chain by its representation: totally ordered and either a machine integer or an enumeration (both finite by construction). bool, Ternary, int qualify; Cardinality and the dense carriers do not
RIsFiniteLSet	The Pst fragment: an L-set whose carrier is a finite chain (IsFiniteChain), so χ is a finite table and normalisation by evaluation is complete. Products of finite chains follow with IsProduct
RIsQuotient	The categorical witness of a regular epimorphism q: A ↠ Q — the dual of IsSubobject
RIsPredicatePair	Two predicates over one object, answering in one species: the operand sort of the predicate combinators below, which close on IsPredicate. Named so the set grammar's && / || (sets) can take exactly the other pairs of terms (relational fragments, mixed terms, the structured collapse) without overlapping these
RIsPeriodic	Taxonomic Decorator: Certifies that an operation is circular (wraps). This is the "Safety Certificate" for machine totality
RIsSaturating	Taxonomic Decorator: certifies that an operation reaches out-of-range values via a saturating escalation (e.g.\ \(\pm \aleph_0\)) rather than wrapping or being undefined
RIsClosedUnder	(S, Op) is closed under a binary operation: Op{}(s_1, s_2) returns a value of type S for any S-typed operands. The textbook closure axiom expressed structurally — no opt-in trait needed because closure is deducible from the operator's signature
RIsClosedUnderUnary	Unary closure variant: Op{}(s) returns S for any S-typed operand. Cardinality has no IsClosedUnderUnary for std::negate<> (negation of a positive natural would need to land outside ℕ); that's the structural witness that -Cardinality is closure-forcing rather than closed
RIsClosedUnderEither	(T, Op) is closed under Op, where Op may be either binary or unary. Distinct from IsClosedUnder (binary) so call sites that need a specific arity stay typo-proof
RIsConstructed	D declares a construction: a base and the shape of its ×
RCommutativeRingLaws	The base's laws that a multiplied-out × rests on
RIsTotal	The Master Safety Certificate for Level 0: is_total, as a concept
RIsTotalArrow	A Morphism whose domain species admits no undefined (hazard) values
RIsPointed	A type T has a chosen identity element under operation Op
RIsMagma	T × T → T (The Base Total Species)
RIsUnitalMagma	A Magma with a global Identity (0 or 1)
RIsInvertible	A pointed (T, Op) where every element has an Op-inverse
RIsLoop	A UnitalMagma with Inverses (-x)
RIsSemigroup	An Associative Magma
RIsCommutativeSemigroup	An Associative Magma where the operation is also commutative
RIsMonoid	A Semigroup with a two-sided Identity element
RIsMonoidHomomorphism	A map between two monoids, (T, Op) and its image under Op2, that carries the operation, declared on every pair, and the unit to the unit, computed (:morphism's PreservesUnit)
RIsCommutativeMonoid	A Monoid where the operation is commutative
RIsGroup	A Monoid with two-sided Inverses (The Perfect Symmetry)
RIsAbelianGroup	A Commutative Group
RIsCyclicGroup	A cyclic abelian group: the honest concept name for \(\mathbb{Z}/n\mathbb{Z}\) carriers and their machine-backed cousins
RIsRig	A Semiring without Negatives (Addition is a Monoid)
RIsRng	A Ring without Identity (Multiplication is a Semigroup)
RIsSemiring	Alias for IsRig: a general multi-operation species
RIsRing	The Perfect Species (Rig ∩ Rng)
RIsCommutativeRing	A Ring whose multiplication is commutative
RIsField	The axiomatic field witness — a commutative ring whose multiplicative structure is an abelian group (zero excluded, by convention on is_invertible_v)
RIsJoinSemilattice	A Semilattice used as the "join" (least upper bound / ∨) half of a Lattice. In bool this is logical_or; in int it is max
RIsMeetSemilattice	A Semilattice used as the "meet" (greatest lower bound / ∧) half of a Lattice. In bool this is logical_and; in int it is min
RIsLattice	Compatibility alias for order-lattice refinement
RIsDistributiveLattice	Compatibility alias for distributive order lattices
RIsBoundedLattice	A IsLattice whose join and meet each carry an identity: the bottom \(\bot\) (unit<T>(Join{})) and top \(\top\) (unit<T>(Meet{}))
RIsBooleanAlgebra	The top of the Boolean-algebra variety Alg(∨,∧,¬,⊥,⊤): a complemented distributive bounded lattice — the ∨/∧/¬ analogue of IsField topping the (signature-expanded) ring variety
RHasClosureForcingShape	Structural shape: Op{} sends (A, A) → B (binary) or A → B (unary) with A ≠ B. Pure deducible clause of IsClosureForcing. The universal-property side — that B is the smallest carrier closing Op over A — is carried by the is_closure_forcing_v opt-in trait below
RIsClosureForcing	Composite: structural shape + opt-in canonicality. The full witness that Op is the closure-forcing operator A → B (or A × A → B), with B the canonical recipient
RIsCopies	A range of n copies of one value, Bird's replicate n x, whose fold under a monoid is the power \(x^n\); n and the value known without walking it: copies_count(r) and copies_value(r), which each model supplies, declared above so that ordinary lookup finds them for models outside this namespace, the standard's among them
RFractionBacking	An integer backing over which fraction arithmetic obeys ℚ's laws under Op: it does not wrap, so a wrapped intermediate cross-product cannot silently break a law. Either it is exact, or it saturates and offers the is_finite hook (RejectsNonFinite) through which ℚ's tripwire rejects the saturated value instead of clamping
Nsets
Ndetail
RStdSetLikeOf
Ndetail_recursion_witness
RFormsNonDescendingRecursion
RFormsDescendingRecursion
RFormsSamePointRecursion
RFormsCyclingRecursion
RFormsMeasuredRecursion
RIsPairing	A carrier that is the product of its two legs and is built from them (the pairing ⟨a, b⟩): a set over it answers r(a, b) as r(⟨a, b⟩) (#1047). IsProduct, plus construction from the legs: std::pair, Complex (ℂ ≅ ℝ×ℝ) and Rational (the pairing then the quotient ℤ×ℤ → ℚ, so r(n, d) asks whether n/d is a member)
RHasSetComplement	A set with a set complement: ~s is formed (the reducer's Not node, or a type's own closed-form complement)
RIs𝔸	A universe: the terminal object of Sub(T) — the reified type constraint 𝔸<T,L,C> itself (carrier, logic, cardinality class)
RIs𝔸Of	U is the universe leg of S: a universe over the same carrier under the same logic
RIsSetObjectLeaf	The leaf case: a set object that carries the subobject surface itself (Definition Lwv) together with its two legs
RIsSetObject	An object of the category Set: a leaf carrying the subobject surface and its legs, or a lattice node — Meet / Join / Not — over set objects on one carrier. The node case is structural: the node's χ is the pointwise evaluation category:lattice already gives it (an arrow into Ω), its universe is its operands', its classifier is the node itself. This is the opaque arm, "the AST is the set", without any set semantics in the lattice partition: the member shape, the inclusion ι and the pullback / pushout apex legs are a sets-side view (as_pullback / as_pushout in :expressions), not a property of the node. The same-logic requirement of the leaf surface is not imposed on nodes: Ø<T,Kleene> ∧ S<T,Boole> is a set object whose reduction the bounded law and the codomain leg decide
RHasUpperBound	ETCS-aligned upper bound for meet/intersection cardinality
RIsCardinality
RIsCountable
RIsFinite
RIsExtensional
RIsWrappingWord	A machine word that is the wrapping ring ℤ/2^w: an unsigned built-in integer (not bool) that the category registrations certify as a commutative ring under + and *, periodic under +, and totally ordered
RIsRingIntegral	The old name of IsIntegerChain, which never claimed a ring
RHasDecidableMembership	S's membership map ranges into two-valued (classical) logic
RIsDecidableSet	A Boolean-valued L-set: an IsLSet whose membership is decidable (χ factors through the dominance Σ ↪ Ω; logic_species is Boole)
RHasCardinalityType	The cardinality bound a comprehension inherits: the datum's when it declares one, else the base's
RIsDatum	A datum over T: a predicate on T (an arrow into a truth object) that is not itself a set. Point, Bounds, LowerCut
RPlainSet
RHasStructuredAnd	Downstream specialization hook for structured predicate conjunction
RHasStructuredOr	Downstream specialization hook for structured predicate disjunction
RIsLogicalTerm	A term of the set grammar, the operand sort of && / ||: an arrow (a predicate, a set, a node over arrows) or a point-free relational fragment (π_1 ⋈ π_2, tagged is_rel_predicate, which meets its domain only at the former &). A bare truth value is not a term: bool && bool stays the host language's, and a constant beside a predicate lifts through :topoi
RSetShaped	A set-shaped carrier: exposes the ambient Domain and the logic_species. The gate constraint for the power-set customization point; the ordered specialisation conjoins it (so it subsumes this gate and wins by partial ordering for the carriers it handles)
RStdSetLike
RNatZedPair	The two carriers of the one cross-carrier pair the library ships, ℕ ↪ ℤ on the variant proxies: A is a set object over Cardinality, B one over SignedCardinality, in the same species. Any set object qualifies (a halfspace, a comprehension, a node): only χ is read
RHeterogeneousPair	Two set objects on different carriers (the ℕ / ℤ pair aside): the operands of a sum
RIsWhereClause	Quantifiers over a finite carrier, decided by type through the finite quotient rather than by enumeration
RWellFounded	A carrier a descent terminates on: the unsigned words, ℕ's shadows, with 0 at the bottom. (Cardinality joins once its monus is a term.)
RHasTermValueAt	A term with a value at the points X: term_value(t, x) is formed
RBindsAt	A term that binds at the points X: bind_check<X>(t) is formed
RComparesEqualTo	The equality atom {x : T | x == pivot}, the datum of the pure equality theory, the one leaf every regular carrier offers (a point in ℂ is this). On a chain the cut subsumes it, x == p ⟺ x ≥ p ∧ x ≤ p. The pivot is a value; the set is Finite whatever the species
RIsRelPredicate	A relational predicate: a predicate on the points of a product (or of a carrier, for an atom on π), tagged is_rel_predicate; it meets its universe only at the former &
RIsTerm	A term of the grammar
RIsConstant	A value that can stand as a constant beside a term: copyable, with state, and not itself part of the grammar (a term, a predicate, an arrow, or an empty tag). The term test comes first, so asking this of a carrier never asks for the carrier's own equality
RTermOperands	The operands of an operator of the grammar: at least one term, the other a term or a constant
REmbedsInto	A value of the sort D is read in the sort C: the same sort, or a truth chain along the dominance into C's species (𝔹 ↪ K₃, the registered lift_logic). The one coercion of the grammar; any other pair of carriers meets through an arrow applied, never implied
RIsGraphAtom	An atom that is the graph of a function of the first slot
Norder
Ndetail_axis	A meet of cylinders: the factor on axis I is the intersection of both children's factors on that axis, so two bounds on the same axis (π_1<=5 && π_1<=3) meet to the tighter one rather than dropping either
RIsUniversalBoundary	A factor that does not constrain its axis: the universal boundary
Ndetail_position
RHasLatticeBottomValue	Whether the carrier registers its lattice bottom (top) under <= as a value, as the machine words do
RHasLatticeTopValue
RIsSuccessor	The algebraic S: T -> T mapping via the Unit element
RIsArchimedean	The scale axiom: Every element can be 'reached' by the Successor. FIXME: misnamed. "Every element reached by the successor" is Peano's and Dedekind's generation of the naturals from one element and a step; the Archimedean property is another axiom, that for x, y > 0 some n has n x > y [1]. Rename to the property it states, and reconcile its algebraic IsSuccessor (x + 1) with the NNO step of dedekind.category (successor, HasNNOStep), which every shipped carrier provides and IsSuccessor's carriers withhold
RIsDiscrete	A set where every point is isolated by a step: the carrier provides the NNO steps (successor / predecessor, HasNNOStep), as the machine integers and the ℕ / ℤ proxies do. The step is the honest discreteness signal; the IsSuccessor leg of IsArchimedean is withheld on every shipped carrier and cannot carry the guard
RIsDense	A property where a midpoint always exists (a < c < b)
RIsDividableChain	A Totally Ordered species with a partitioning algorithm (/)
RIsDedekindComplete	The topological "Soul" of the Continuum (LUB property)
RIsStepTerm	A set term whose normal form the run lists read
RSubobjectLatticePair	A compatible pair of subobject lattices — same ambient Domain and logic_species: the canonical rung on which subset is defined. Ties the order to category::IsSubobjectLattice rather than a bespoke shape; the same-logic clause is the cross-logic-mereology guard (#833 review)
RDecidableMeetSubset	\(A \subseteq B\) is decidable via the structural meet: a subobject-lattice pair whose meet-then-equality is a truth value. The gate for the generic identity <=; where the meet does not collapse this is unsatisfied (the honest exists / forall wall) and a per-carrier <= must supply the case
RHasSubset	A decidable <= exists for the pair — generic (meet) or a per-carrier specialisation (Singleton membership, Interval endpoints). The gate for the derived relations, so they ride any <=, not only the meet-based one
RHasProperSubset	HasSubset plus a bool ==, so \(A \subsetneq B \equiv A \subseteq B \wedge A \neq B\) is expressible
RHasLatticeOperators	Pure syntactic shape: T supports the bitwise / lattice operators &, |, ^, ~ with results convertible to T
RIsOrderMeetSemilattice	Re-export the certified meet-semilattice stage from :posetal
RIsOrderJoinSemilattice	Re-export the certified join-semilattice stage from :posetal
RIsOrderLattice	Bundled lattice witness: the strict commutative-ring proof under (std::bit_xor<T>, std::bit_and<T>) AND the bitwise/lattice operator surface on T, by definition
RIsOrderDistributiveLattice	Re-export the certified distributive lattice stage from :posetal
RIsPreOrdered	The most basic relation: Reflexive and Transitive
RIsDirectedSet	A Pre-ordered structure where any two elements have a common successor
RIsPartiallyOrdered	A refinement of the Pre-Order that satisfies Antisymmetry (Identity)
RIsDirectedPoset	The "Convergent Identity": A Poset that is also a Directed Set
RHasPartialOrderOperators	Pure syntactic shape: T supports the partial-order operators <, <=, >, >= with results in the truth-value carrier L::Ω of a chosen logical species
RHasPartialOrderOperatorsWith	Heterogeneous shape: T and U can be compared via the four partial-order operators in both directions, yielding results in the truth-value carrier L::Ω
RSubReifiable	A base that reifies as an ordered-carrier subobject Sub(C): it is SetShaped, its carrier is totally ordered (the enabler — so the gate itself, not a later membership call, rejects an unordered carrier), and it coerces to Sub via one of the converting constructors above. The single gate concept for both power_set and 𝔓 (DRY), and — because it conjoins the very SetShaped atom the :sets default is constrained on — it subsumes that deleted gate, so it wins by partial ordering for the ordered families
RIsStepSource	A step source: the carrier and species, the value before every step, and the steps as a forward range, in order along the chain
RIsStrictWeakOrder	The standard C++ 'Compare' requirement (e.g., for std::sort)
RIsTotallyOrdered	A refinement where every pair is comparable (The Chain)
RIsLinearOrder	Synonym for Total Order
RHasTotalOrderOperators	Pure syntactic shape: T supports the spaceship operator <=> alongside the four partial-order operators (the latter return L::Ω)
RHasTotalOrderOperatorsWith	Heterogeneous shape: T and U can be compared via <=> in both directions, alongside the four partial-order operators (the latter return L::Ω)
Nanalysis
Ndetail
RIsNumericalBridgeScalar
Rdual_admits
RIsDifferentialForm	A mapping from a Tangent Space to a Scalar
RIsHamiltonian	Formal verification of the energy mapping
RIsPoissonAlgebra	A Ring equipped with a bracket satisfying the Jacobi Identity
RIsKernel
Ngeometry
RHasFiniteDimension	A vector type whose coordinate index set is finite
RHasCountableDimension	A vector type whose coordinate index set is at most countably infinite
RHasDimension	A vector type with a specific compile-time dimension N
RIsAffine	Affine-space witness over scalar carrier S
RIsMetricSpace	A set equipped with a distance function (metric) d(a, b)
RIsEuclideanSpace	A Vector Space that is also a Metric Space where distance is the Norm
RIsFunctionSpace	W is a function space T^D — eval f(d), pointwise +, and scalar · over T
RIsFiniteDimensionalInnerProductSpace	A finite-dimensional real inner-product space
RIsHilbertSpace	An Inner Product Space where every Cauchy sequence converges
RHasInnerProduct	Carrier exposing a scalar-valued inner-product form, its exact squared norm abs2, and the (√-induced) norm
RIsInnerProductSemimodule	A semimodule equipped with an inner-product-like scalar form
RIsInnerProductModule	A module equipped with an inner-product-like scalar form
RIsInnerProductSpace	A field-like vector carrier equipped with an inner product morphism
RIsGeometricLattice	A Set S whose elements are integer-coordinate points, embedded into a continuous vector space V via a declared-monic arrow E
RIsMatrixScalar	A scalar type that can serve as coefficients in a LinearMap
RHasMatrixScalarEmbedding	Floating carrier that is admissible as a matrix scalar by policy
RHasJacobianAt	Map-like object exposing a finite-dimensional LinearMap Jacobian
RIsOuterProductSpace	W carries the outer-product structure for factor spaces U and V: there is a dyad(u, v) → W constructor representing u ⊗ v in W
RIsTangentBundle	A flat-case (element-wise) tangent-bundle carrier over a base scalar: a pair (point, tangent vector) with ring-shaped arithmetic
RIsLinearMapModule	Verify that LinearMap<F, R, C> behaves as a module over scalar F
Nieee
RIsIEEEPropagationOp	Category-grounded contract for propagation operation tokens
Nlinear_algebra
RRankNullityWitness	Static witness for the rank-nullity identity
RLinearOperatorContract	Minimal contract for finite-dimensional linear operator carriers
RHasDimensionCount	A carrier exposing a compile-time dimension count (axes or slots)
RHasOrientation	A carrier that declares whether it is a column or a row
RIsColumnVector	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
RIsCovector	A row vector / covector: the RowOrientation twin of IsColumnVector — an IsSemimodule row
RHasMatrixShape	A matrix carries two dimensionalities: row count and column count
RHasColumnType	A matrix exposes its columns as a concrete vector carrier
RHasRowType	A matrix exposes its rows as a concrete covector carrier
RHasColumnDecomposition	A matrix can be viewed as the horizontal concatenation of its column vectors
RHasRowDecomposition	A matrix can be viewed as the vertical concatenation of its row vectors
RIsMatrix	The structural-matrix slogan-pack: shape + column/row types + both decompositions
RIsMatrixSubmoduleLike	Matrices over a ring form at least a submodule-like carrier
RIsMatrixAsModule	The strict "sometimes a module" witness
RHasMatrixMultiplication	Square-matrix multiplication: M × M → M
RHasTranspose	A matrix carrier equipped with a transpose operation
RHasInvolutiveTranspose	Transpose is its own inverse at the type level: decltype((a.transpose()).transpose()) is M
RIsTransposeDualPair	V and Covec are dual under transpose: V → Covec and Covec → V, with both round-trips returning the original type
RIsMatrixOverFieldRingLike	Matrices over a field carry at least a ring structure plus transpose
RHasMultiplicativeInverse	A matrix carrier with a closed-form inverse operation
RIsInvertibleMatrixOverField	A matrix over a field that carries ring-like structure plus an .inverse() operation
RIsOrthogonalMatrixCarrier	Carries the operations under which the orthogonality law Mᵀ · M = I makes sense
RMatchesAdditiveShape	Two matrix-like carriers can be added iff they share shape and scalar type
RMatchesMultiplicativeShape	Two matrix-like carriers can be composed iff the inner dimensions agree: A::column_count == B::row_count and the scalar types match
RHasConformingMatrixAddition	A and B support shape-conformant addition, and the result has the same shape and scalar type
RHasConformingMatrixMultiplication	A and B support shape-conformant multiplication, and the result has shape A::row_count × B::column_count
RIsMatrixAlgebra	Umbrella concept bundling all 9 matrix slogans for square matrices over a field
RIsDimension	A type-template witness for a dimension cardinality. Today's inhabitants: dim_finite<N> and dedekind::sets::ℵ<N>
RIsLinearOperator	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)
Nmorphologies
RIsCyclic	\emph{Operational} duck-typed check that T carries the member API of a cyclic structure: T::Domain alias, T::generator() returning a Domain element, and T::successor(a) walking the chain
RIsSimplyInfinite
RIsCyclicRing
RIsOrderedField
RIsArchimedeanField
RIsDedekindCompleteField
RIsMinkowskiSummable
RIsInteger
RIsSaturatingInteger	Saturating-ℤ-shape integer: integer surface + translation-invariant order (sentinels propagate cleanly; no cyclic wrap). The variant ℤ proxy SignedCardinality is the canonical witness
RIsCyclicInteger	Cyclic-ℤ-shape integer: integer surface + abelian-group-cyclic under +. SignedExtensionalCardinal<> (sign-magnitude ℤ/2^{N*64}ℤ) is the canonical witness via IsCyclicGroup<SignedExtensionalCardinal<>, std::plus<>> pinned in :sets:cardinality
RHasEuclideanGcd
Nnumbers
RIsIEEEPropagationOp
RIsComplexScalar
RIsEscapeCriterion	Escape predicate: ComplexType → bool
RIsNatural	Structural concept for a commutative semiring with total order (the intensional ℕ)
RIsQuaternionScalar	Scalar type suitable as quaternion components
RRejectsNonFinite	The rejection contract a saturating backing must offer ℚ's tripwire: is_finite(i), found by ADL, says whether i is a point of ℤ or a sentinel (±ℵ_0 / NaZ). Rational rejects a non-finite value wherever one can arise (construction, comparison); a saturating carrier without this hook would clamp silently and is not admitted as a backing (see FractionBacking)
RIsRational	Q is the rational field Rational<Z> — the canonical exact, dense, strongly-ordered coefficient carrier. Used to gate the real carriers (Cut, QuadraticReal): over \(\mathbb{Q}\) a nonsquare integer D has \(\sqrt D\notin\mathbb{Q}\) (a theorem), so those carriers are genuine (canonical representation, sound conjugate/norm) — which fails for a coefficient field that already contains \(\sqrt D\) (e.g. the degenerate QuadraticReal<2, QuadraticReal<2>>)
RIsIntegralScalar	Numbers-layer alias for the algebra scalar bridge concept
RIsUnsignedIntegralScalar	Numbers-layer alias for the algebra scalar bridge concept
RIsFloatingScalar	Numbers-layer alias for the algebra scalar bridge concept
RIsScalar
RIsNumbers	The Root Category for all Numerical Structures
Nsequences
RIsCauchySequence	A Seq is a Cauchy sequence: its tail is eventually arbitrarily small under the metric on the carrier
RIsConvergentSequence	A Cauchy sequence whose limit can be witnessed via limit(s)
RIsClassicallyConvergent	A Cauchy sequence whose carrier sits in the classical logic regime, so the Cauchy ⇒ convergent collapse (limit extraction) fires honestly
RIsOrderConvergent	A sequence that converges in the order sense: \(\liminf_n s(n) = \limsup_n s(n)\), with \(\liminf = \bigsqcup_n \bigsqcap_{k\ge n} s(k)\) and \(\limsup = \bigsqcap_n \bigsqcup_{k\ge n} s(k)\)
RIsSeries	A sequence whose Codomain carries the additive structure needed to form partial sums \(S_n = \sum_{k\le n} a_k\)
RIsSummable	A convergent series. Necessary condition (the engineer's obligation to respect): summable ⇒ a_n → 0. The runtime numerical hooks ratio_test_converges, root_test_converges, comparison_test_converges, and converges_series_partial_sums (below) are the operational counterparts that decide summability for concrete float carriers
RIsAbsolutelyConvergent	An absolutely convergent series. Refines IsSummable: in a complete (Banach) carrier absolute convergence implies convergence, so an IsAbsolutelyConvergent witness is also IsSummable — the same refinement shape as IsConvergentSequence over IsCauchySequence. Carrier completeness is the honesty obligation that makes the implication sound; the witness opts into both traits
RIsBoundedSequence	A sequence whose image is order-bounded. Bishop §2
RIsMonotoneSequence	A monotone sequence. Bishop §2; together with IsBoundedSequence drives the monotone-convergence upgrade (LEM-gated, #719 Slice 5)
RIsPeriodicSequence	A period-N sequence. Honest-Rejection foil for the monotone / Cauchy rows (a non-constant periodic sequence is bounded but neither monotone nor Cauchy)
RIsAbsorptiveSequence	An eventually-constant sequence. The simplest convergent case (limit = the absorbing value); period-1-eventually dual to IsPeriodicSequence
RIsSubsequence	Sub is a subsequence of Sup (same Codomain, strictly increasing index map). Feeds the Bolzano-Weierstrass row (#719 Slice 5: every bounded sequence has a convergent subsequence)
RWitnessesBolzanoWeierstrass	The Bolzano–Weierstrass crown: Sub witnesses that the bounded sequence Sup has a convergent subsequence
RIsCurve	A real-parameter indexed morphism family
RHasLimit	Species that can resolve a Path into a single point
RIsIndexedMorphismFamily	A category arrow equipped with explicit index cardinality metadata
RIsCountablyIndexedFamily	An indexed family whose index magnitude is finite or countably infinite
RIsNet
RIsSequence	The fundamental mapping from a Domain Set to a Value Type
RIsFiniteSequence	A sequence bound by a Finite Domain
RIsCountableSet	A Set capable of producing a Path (Enumerability)
RIsTerminalSet	An Enumerable Set with a known Terminal Index
RIsStreamComonad	\emph{Operational} duck-typed check that W carries the Uustalu–Vene stream-comonad shape on an infinite sequence \(\mathbb{N} \to A\). The concept body checks the two primitive legs — ε (head w.at(0)) and δ (tails(w)) — only; the third leg extend (w <<= f) is the derived \(\mathrm{map}\,f \circ \delta\) and is certified separately by the IsCoKleisliTriple witness (pinned beside the IsStreamComonad<Path<int>> assertion below), not re-checked here
RIsPstSet	A decidable set object over a finite chain with the covering step: a leaf or a lattice node whose χ answers in \(\mathbb{B}\) (the Δ grade). An L-valued set enters through its α-cuts
RHasPrefixBound	A relation is bounded (composable over a finite middle) iff its predicate carries a prefix_bound
RIsEventuallyPeriodic	Seq has a finite-state (lasso) presentation: a lasso_presentation specialisation giving a positive period and a pre_period. This is the finite-presentation witness that licenses a decidable, structural-recursive tail-equivalence test (see decide_tail_equivalence)
Noptimization
RHasCriticalPathStep
RSuitableForAxisAlignedFastPath	Carrier requirements for the bit-ops fast-path kernel
RHasUnitRangeEntries	Pack-level concept: every halfspace has entries in {−1, 0, +1}
RIsAxisAlignedPolytope	Pack-level concept: every halfspace is axis-aligned
Nrelational
Ndetail_rows
RHasCarrierConstant	The constant type K has its own hook for a carrier's value c: carrier_constant, found by argument-dependent lookup
RIsRelation	Concept: a set S whose ambient type is std::pair<T1,T2> is a valid binary relation on T1 and T2
RIsPairLike	Pair-like carrier: both coordinates present — the shape every relation (converse, reflexive, symmetric, is_relation) assumes
RIsFunctional
RIsEntire
RIsFunction
RIsGraph
Ntopology
RHasDiscreteCarrier	The set's carrier is a discrete chain, so its order topology is the discrete topology — and there every subset is clopen
RIsOpen	A set where every point has a neighborhood entirely within the set
RIsClosed	A set that contains all its limit points — in the carrier's order topology. Same three-leg inference as IsOpen
RIsClopen	A set that is BOTH open and closed — the topological face of decidability
RIsNeighborhood	A set that "surrounds" a point p
RIsConvex	A Set that satisfies the convexity theorem (no holes)
RIsConvexMagmoid	Convex sets form a Magmoid under the intersection operation
RIsTruthChain	A truth chain the queries can read: a Pst carrier that is finite by its representation and has the covering step
RIsNaturalTransformation	α : F ⟹ G