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: if the schema declares an instantiable (non-abstract) concept S <: Parent that specializes none of the members, the cover is provably incomplete and the build is refused (OE0242) — 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, so 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.

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).