Group axioms — disjoint, complete, partition
A group axiom constrains a set of sibling concepts collectively: that they never overlap, that they jointly exhaust a parent, or both. The three forms share one declaration shape — a contextual keyword, an optional parent, and a brace list of member concept paths:
disjoint { Cat, Dog, Fish } // pairwise non-overlapping
complete Animal { Cat, Dog, Fish } // jointly exhaustive over Animal
partition Animal { Cat, Dog, Fish } // disjoint AND complete
The keywords (disjoint / complete / partition) are contextual — they lex as ordinary identifiers and bind as group-axiom keywords only in declaration position followed by the group-axiom shape, so they remain available as concept and field names elsewhere. A group axiom introduces no name of its own; it names existing concepts.
disjoint { A, B, C } asserts the members are pairwise non-overlapping: no individual is an instance of two of them at once. Disjointness is instance-level. A write that would classify one individual into two declared-disjoint members is refused (OE0240), so the contradictory state never enters the store. disjoint takes no parent — the members need not share a supertype.
complete Parent { A, B, C } asserts the members jointly cover Parent: every Parent instance is an instance of at least one member. Under the closed-world default (Type system), a Parent instance derivable into none of the members is an uncovered instance, and the write that creates it is refused (OE0241). Each member must be a subtype (<:, transitively) of Parent, checked at elaboration (OE0243 otherwise). Completeness has a second, static half, but it fires only when uncoveredness is provable. The build is refused (OE0242) when the schema declares an instantiable (non-abstract) concept S <: Parent that is provably disjoint from every cover member — so no individual can be both an S and a member (for instance because a disjoint/partition declaration separates S from each member, or because the cover is empty). A subtype that merely fails to be a static subtype of any member is not refused: under multiple classification an S individual can still be classified into a member at write time, so its covering is left to the runtime OE0241 guard. (This is why orthogonal generalization sets over one class — two partitions of Parent along independent dimensions — are admitted: a member of one is not disjoint from the members of the other.) An abstract subtype, having no direct instances, is exempt. This static gate ranges only over the concepts declared in the same file as the group axiom; a subtype introduced in another module is not seen at this point, and — like an in-file subtype that is not provably uncovered — its covering is left to the runtime OE0241 guard rather than refused statically.
partition Parent { A, B, C } is the conjunction: the members are both disjoint and complete over Parent. It imposes the OE0240 overlap guard, the OE0241 covering guard, and the OE0242 / OE0243 static gates together.
A declared disjointness also constrains typed-slot writes, because it makes a slot’s demand unsatisfiable rather than merely unmet. Writing into a relation endpoint, or into a concept-typed field, an individual already classified under a concept declared disjoint from the slot’s declared concept is refused: classifying that individual under the slot’s concept would itself violate the group, so the write can never be satisfied in this state or any later one. The refusal fires at elaboration where the value’s concept is statically known (OE1426 endpoints, OE1434 fields) and at write time against the individual’s real classification (OE1428 endpoints, OE1435 fields). It does not depend on the slot concept’s world assumption — an open world permits membership that is unknown, not membership a declaration forbids. Two concepts with no declared disjointness are unaffected: multiple classification is legal, an individual under one may later also be classified under the other, and the write stands.
Disjointness and covering are enforced as ordinary substrate checks (Rule atom — fn, derive, query, mutate, check) the compiler synthesizes from the declaration — one overlap check per unordered member pair, one negation-as-failure covering check per cover — so a violating write is refused by the same delta-guard that enforces a hand-written check, with no separate axiom machinery. The covering check is closed-world: it fires when no member membership is derivable. Its interaction with a concept’s #[world(open)] assumption is specified in World assumptions (CWA / OWA) (RFD 0045).
A degenerate group axiom synthesizes no runtime check, because it has nothing to guard. An empty disjoint { } and a one-member disjoint { A } have no unordered pair to overlap, so no overlap check is produced and the declaration is accepted in silence. An empty complete Parent { } likewise produces no covering check — but it still meets the static cover gate above, so any instantiable subtype of Parent (including Parent itself, if non-abstract) is then provably uncovered and the build is refused (OE0242).