Trait ConditionSliceExt 

pub trait ConditionSliceExt {
    // Required method
    fn iter_kind(&self, kind: ConditionKind) -> KindMatches<'_> ;

    // Provided methods
    fn find_kind(&self, kind: ConditionKind) -> Option<&Condition> { ... }
    fn has_kind(&self, kind: ConditionKind) -> bool { ... }
    fn count_kind(&self, kind: ConditionKind) -> usize { ... }
    fn distinct_kinds(&self) -> Vec<ConditionKind> { ... }
    fn iter_distinct_kinds(&self) -> impl Iterator<Item = ConditionKind> + '_ { ... }
    fn distinct_kind_count(&self) -> usize { ... }
    fn missing_kinds(&self) -> Vec<ConditionKind> { ... }
    fn iter_missing_kinds(&self) -> impl Iterator<Item = ConditionKind> + '_ { ... }
    fn missing_kind_count(&self) -> usize { ... }
    fn first_distinct_kind(&self) -> Option<ConditionKind> { ... }
    fn first_missing_kind(&self) -> Option<ConditionKind> { ... }
    fn last_distinct_kind(&self) -> Option<ConditionKind> { ... }
    fn last_missing_kind(&self) -> Option<ConditionKind> { ... }
    fn is_kind_saturated(&self) -> bool { ... }
    fn is_kind_empty(&self) -> bool { ... }
    fn is_kind_partially_covered(&self) -> bool { ... }
    fn has_any_distinct_kind(&self) -> bool { ... }
    fn has_unique_distinct_kind(&self) -> bool { ... }
    fn unique_distinct_kind(&self) -> Option<ConditionKind> { ... }
    fn has_multiple_distinct_kinds(&self) -> bool { ... }
    fn has_at_most_one_distinct_kind(&self) -> bool { ... }
    fn has_any_missing_kind(&self) -> bool { ... }
    fn has_unique_missing_kind(&self) -> bool { ... }
    fn unique_missing_kind(&self) -> Option<ConditionKind> { ... }
    fn has_multiple_missing_kinds(&self) -> bool { ... }
    fn has_at_most_one_missing_kind(&self) -> bool { ... }
    fn lacks_kind(&self, kind: ConditionKind) -> bool { ... }
    fn has_only_kind(&self, kind: ConditionKind) -> bool { ... }
    fn lacks_only_kind(&self, kind: ConditionKind) -> bool { ... }
    fn has_multiple_of_kind(&self, kind: ConditionKind) -> bool { ... }
    fn has_unique_of_kind(&self, kind: ConditionKind) -> bool { ... }
    fn has_at_most_one_of_kind(&self, kind: ConditionKind) -> bool { ... }
    fn unique_of_kind(&self, kind: ConditionKind) -> Option<&Condition> { ... }
}

Slice-level (ConditionKind, presence) probe on any &[Condition] — the ONE substrate primitive that owns the .iter().any(|c| c.kind == K) walk shape both current production sites hand-authored past the ★★ PRIME-DIRECTIVE ≥ 2 duplication threshold. Callers compose the two-half union at their site (Boundary::has_condition_kind on preconditions ∪ postconditions) or on ONE half only (the ephemeral require-tag classifier’s closed-loop-auth arm on spec.postconditions) — the primitive owns ONLY the per-slice walk, so the composition choice stays typed at the caller.

Why lift

Pre-lift the .iter().any(|c| c.kind == K) walk lived hand-authored at THREE production sites: twice inside Boundary::has_condition_kind’s union (pre + post), once at evaluate_ephemeral_require_tag’s closed-loop-auth arm in tatara-reconciler::bin::tatara-check (with matches! sugar instead of ==, but the same predicate). The (&[Condition], ConditionKind) → bool shape is the substrate primitive: a future consumer that walks a Vec<Condition> (a coherence check that verifies “every ClosedLoopAuth postcondition carries an issuer param key”, an editor completion listing which ConditionKind arms appear on ONE side only, a hypothetical postcondition-<kind> require-tag prefix family that dispatches on postconditions alone — the peer of the existing condition-<kind> family that dispatches on the pre ∪ post union via Boundary::has_condition_kind) reaches this ONE primitive through slice.has_kind(k) instead of restating the .iter().any closure body.

Sibling to Boundary::has_condition_kind

Same axis, one refinement lower: Boundary::has_condition_kind is the two-slice-union probe; has_kind here is the one-slice probe the union composes twice. A future normalization at the presence probe shape (widening the return to Option<&Condition> for deeper diagnostics, adding a debug-build assertion on redundant duplicates, switching to a linear scan that also counts matches) lands at ONE site here — both Boundary::has_condition_kind + every downstream slice.has_kind(K) callsite pick it up mechanically.

Compounding

Self::find_kind is the widened primitive returning Option<&Condition> that both has_kind (self.find_kind(k). is_some(), the default body) and future diagnostic consumers compose against. A has_kind_matching(|&Condition| -> bool) predicate extension similarly lands as ONE new default method on this trait — the closed-set discriminator case becomes has_kind(k) == self.has_kind_matching(|c| c.kind == k) by construction, so a regression that drifted one from the other becomes structurally impossible past the trait boundary.

Theory anchor: THEORY.md §II.1 invariant 5 — composition preserves proofs; the per-slice walk lives at ONE substrate site so the two-half union in Boundary and the one-half probe on crate::ephemeral::EphemeralSpec::postconditions compose through the SAME primitive. THEORY.md §VI.1 — generation over composition; a future Vec<Condition> consumer reaches the primitive through slice.has_kind(k) with no per-caller restatement of the .iter().any(|c| c.kind == K) closure body.

Required Methods

fn iter_kind(&self, kind: ConditionKind) -> KindMatches<'_>

Returns an iterator yielding every Condition in this slice whose Condition::kind equals kind, in slice order — the ONE widened primitive on the slice-level presence-probe axis that both Self::find_kind (via the default iter_kind(k).next() body) and Self::has_kind (via the transitive find_kind(k).is_some() default) compose against.

Sibling to Self::find_kind

One refinement wider: find_kind collapses the return to Option<&Condition> (yielding only the earliest match); iter_kind returns the whole match stream so callers can count it, collect it into a Vec<&Condition>, ask for the nth element, or compose it with any other std iterator adaptor without re-walking the slice. The default body of find_kind is self.iter_kind(kind).next() — the two methods share ONE walk semantics by construction, so a regression that drifted the first-match probe from the widened stream becomes structurally impossible past the trait boundary.

Semantics

Yields &c for each c in this slice with c.kind == kind, in slice order — a slice that carries multiple matches yields each in turn (the composition law find_kind(k) == iter_kind(k).next() binds the first match to the earliest position). An empty slice, or a slice with no matching kind, yields nothing. Byte-for-byte equivalent to self.iter().filter(|c| c.kind == kind).

Compounding

A future coherence check that verifies “each ConditionKind appears at most once per side” reads slice.iter_kind(k).nth(1).is_none() at ONE call site rather than restating the count-with-filter closure body. A future diagnostic that enumerates every match of a kind (an operator-facing “3 PromQL preconditions matched” message, an audit dump listing every match of a repeated kind) reaches this ONE primitive through slice.iter_kind(k).collect() rather than re-walking the slice with .iter().filter(...) at the callsite. The presence-probe axis now carries three refinements (bool via has_kind, Option<&Condition> via find_kind, impl Iterator<Item = &Condition> via iter_kind) at ONE typed algebra surface — every downstream consumer picks the coarsest one that answers its question and the coarser ones stay compositionally derived from this primitive.

Provided Methods

fn find_kind(&self, kind: ConditionKind) -> Option<&Condition>

Returns the first Condition in this slice that carries the given ConditionKind, or None if none matches. Default body: self.iter_kind(kind).next() — a thin projection of the widened primitive Self::iter_kind onto its first element. The composition law find_kind(k) == iter_kind(k).next() binds the first-match probe to the widened stream at the trait’s default body.

Sibling to Self::has_kind

One refinement wider: has_kind collapses the return to a bool; find_kind returns the matching &Condition so callers can read Condition::params without re-walking the slice. The default body of has_kind is self.find_kind(kind).is_some() — the two methods share ONE walk semantics by construction. Byte-for-byte equivalent to self.iter().find(|c| c.kind == kind).

fn has_kind(&self, kind: ConditionKind) -> bool

True iff at least one Condition in this slice carries the given ConditionKind. Default body: self.find_kind(kind). is_some(). The single-slice presence probe both Boundary::has_condition_kind (twice, in a union) and the ephemeral closed-loop-auth require-tag arm (once, on postconditions only) compose against.

fn count_kind(&self, kind: ConditionKind) -> usize

Number of Conditions in this slice carrying the given ConditionKind — the scalar cardinality refinement on the slice-level presence-probe axis. Default body: self.iter_kind(kind).count() — a thin projection of the widened primitive Self::iter_kind onto its cardinality.

Sibling to Self::iter_kind / Self::find_kind / Self::has_kind

Fourth refinement on the presence-probe algebra: iter_kind yields the whole match stream, find_kind collapses it to the first match, has_kind collapses that to a bool, and count_kind collapses the stream to its cardinality without materializing any intermediate Vec or Option. The composition laws count_kind(k) == iter_kind(k).count(), has_kind(k) == (count_kind(k) > 0), and find_kind(k).is_some() == (count_kind(k) > 0) share ONE walk semantics by construction; a regression that drifted the cardinality probe from the widened stream becomes structurally impossible past the trait boundary.

Semantics

Returns self.iter().filter(|c| c.kind == kind).count() — a slice that carries multiple matches returns that count, an empty slice or a slice with no matching kind returns 0.

Compounding

A future coherence check that verifies “each ConditionKind appears at most once per side” now reads slice.count_kind(k) <= 1 at ONE call site rather than restating either slice.iter_kind(k).nth(1).is_none() or the iter_kind(k).count() <= 1 idiom. A future require-tag classifier arm that surfaces multiplicity to the operator (a hypothetical condition-count-<kind> prefix family that publishes the raw cardinality, an audit dump reporting “3 PromQL preconditions matched”) reaches this ONE primitive through slice.count_kind(k) rather than restating the .iter_kind(k).count() chain body at the callsite. The presence-probe axis now carries FOUR refinements at ONE typed algebra surface — every downstream consumer picks the coarsest one that answers its question and the coarser ones stay compositionally derived from Self::iter_kind.

fn distinct_kinds(&self) -> Vec<ConditionKind>

The set of ConditionKind variants that appear at least once in this slice, projected in ConditionKind::ALL order — the closed-set-inversion refinement on the slice-level presence-probe axis. Default body: ConditionKind::ALL.into_iter().filter(|k| self.has_kind(*k)).collect() — a thin projection over the closed set that composes against Self::has_kind per variant.

Sibling to Self::has_kind / Self::find_kind / Self::iter_kind / Self::count_kind

FIFTH refinement on the presence-probe algebra, distinct in axis from the other four: has_kind / find_kind / iter_kind / count_kind fix a ConditionKind and vary the return type (bool / Option<&Condition> / impl Iterator<Item = &Condition> / usize); this refinement INVERTS the axis by fixing the slice and varying over ConditionKind::ALL, returning the SET of present kinds. The composition law distinct_kinds().contains(&k) == has_kind(k) for every k ∈ ConditionKind::ALL binds the closed-set-inversion probe to the point probe at the trait’s default body.

Semantics — canonical subsequence of ConditionKind::ALL

Returns a Vec<ConditionKind> whose elements appear in ConditionKind::ALL order with no duplicates. A slice that carries the same ConditionKind at multiple positions contributes ONE entry to the returned set (the closed-set projection collapses multiplicity — a caller that needs the per-kind cardinality reaches for Self::count_kind). An empty slice, or a slice with no matching kind under any ConditionKind::ALL variant, returns an empty vec.

Why closed-set-inversion is a distinct axis

The other four refinements answer “for THIS kind, how does the slice populate the probe’s return type?”; this refinement answers “for THIS slice, which kinds appear at least once?”. A consumer that needs to enumerate every present kind for an audit dump ("boundary carries [PromQL, ClosedLoopAuth]"), a coherence check that verifies “every process’s boundary carries at least ONE of {JobAttested, ClosedLoopAuth}”, or a require-tag family that surfaces the distinct-set as a whole (condition-kinds-distinct-count) reaches this refinement rather than paying for a per-kind sweep with has_kind at the callsite. The point probe stays composable one axis over (slice.has_kind(k) for a fixed k); the aggregate refinement lives at the same trait, one axis away.

Compounding

A future coherence check that enforces “every boundary carries at least ONE distinct kind” (a warning surfaced when boundary.distinct_condition_kinds().is_empty()) reaches this ONE primitive rather than paying for the eight-way for k in ConditionKind::ALL { if boundary.has_condition_kind(k) { return true; } } sweep at every callsite. A future require- tag classifier arm that publishes the distinct-set cardinality as a scalar (a hypothetical condition-kinds-distinct-<n> prefix family, an audit dump reporting “boundary carries N distinct kinds”) reaches this ONE primitive through boundary.distinct_condition_kinds().len() rather than restating the closed-set-inverted .iter().filter(...).count() idiom at every callsite. The presence-probe axis now carries FIVE refinements at ONE typed algebra surface — the four point- probes fixing a kind AND the ONE closed-set-inversion probe fixing a slice — every downstream consumer picks the one that answers its question and the others stay compositionally derived from the single-source-of-truth widened primitive.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The closed-set-inversion projection lives at ONE substrate site as a typed projection of Self::has_kind over the closed set ConditionKind::ALL. Every downstream aggregate consumer binds through the SAME shape rather than restating the ALL-filter closure body.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically (the closed-set walk picks up the new entry) and every downstream consumer sees the wider set without further per-caller edit.

fn iter_distinct_kinds(&self) -> impl Iterator<Item = ConditionKind> + '_

Zero-allocation iterator peer of Self::distinct_kinds — walk ConditionKind::ALL in canonical order and yield every ConditionKind whose corresponding slot on this slice is populated (at least one Condition with that kind), WITHOUT materializing an intermediate Vec<ConditionKind>.

Default body: ConditionKind::ALL.iter().copied().filter(|&k| self.has_kind(k)). The composition law distinct_kinds() == iter_distinct_kinds().collect::<Vec<_>>() holds by construction — Self::distinct_kinds’s default body IS self.iter_distinct_kinds().collect(), so a caller that overrides the widened Vec primitive with a divergent walk simultaneously drifts both surfaces (surfacing at the substrate testkit assert_slice_refinement_composition_laws which pins the Vec projection equals iter().collect()).

Sibling to Self::distinct_kinds / Self::distinct_kind_count

Load-bearing iterator peer of the slice-level closed-set-inversion axis — where distinct_kinds returns the SET (heap-allocated Vec, canonical ConditionKind::ALL order) and distinct_kind_count scalar-projects its cardinality, iter_distinct_kinds opens the walk as a Copy iterator so consumers that need a short-circuiting fold (.any(|k| pred(k)), .find(|&k| pred(k)), .take_while(|k| pred(k)), .map(|k| project(k))) avoid the intermediate allocation entirely.

Peer to crate::tagged_union::TaggedUnion::iter_populated_kinds

Same shape at the peer axis one struct layer up: where iter_populated_kinds opens the closed-set-inversion walk on the tagged-union parent-level presence-probe axis, iter_distinct_kinds opens the closed-set-inversion walk on the slice-level presence-probe axis. Both close the “load-bearing iterator” refinement at two adjacent typescape sites through the SAME <CLOSED_SET>::ALL.iter().copied().filter(|&k| has_probe(k)) composition body under a POSITIVE point-probe.

Compounding future consumers

• Every scalar closed-set-inversion peer already at the trait (distinct_kind_count, first_distinct_kind, last_distinct_kind, unique_distinct_kind, has_any_distinct_kind) folds a specialization of ConditionKind::ALL.iter().filter(|k| self.has_kind(**k)) — they can compose over iter_distinct_kinds() at ONE substrate site rather than restating the closed-set walk body per peer.
• A downstream diagnostic composer (an operator-facing “boundary carries: [{}]” message that streams the label list into a write! buffer) reads slice.iter_distinct_kinds().map(|k| k.label()) and folds through itertools::join without the allocation Vec<ConditionKind> -> String pays.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The load-bearing iterator projection lives at ONE substrate site; every downstream aggregate consumer refines it through a standard-library iterator fold rather than restating the ConditionKind::ALL-walk closure body.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches the walk mechanically (the closed-set filter picks up the new entry) and every downstream fold sees the wider set without further per-caller edit.

fn distinct_kind_count(&self) -> usize

Scalar cardinality projection of Self::distinct_kinds onto its .len() — the number of ConditionKind variants that appear at least once in this slice. Default body: ConditionKind::ALL.iter().filter(|k| self.has_kind(**k)).count() — a closed-set walk that composes against Self::has_kind per variant WITHOUT materializing an intermediate Vec<ConditionKind>. A slice that carries the same ConditionKind at multiple positions contributes 1 to the count (the closed-set projection collapses multiplicity — a caller that needs the per-kind cardinality reaches for Self::count_kind).

Sibling to Self::distinct_kinds

Scalar projection of the closed-set-inversion widened primitive — where distinct_kinds returns the SET (a Vec<ConditionKind> in canonical ConditionKind::ALL order), distinct_kind_count collapses that set to its cardinality. The composition law distinct_kind_count() == distinct_kinds().len() binds the scalar projection to the widened primitive at the trait’s default body and is swept substrate-wide by assert_slice_refinement_composition_laws as its sixth arm.

Peer to crate::tagged_union::TaggedUnion::populated_kind_count

Same shape at the peer axis one struct layer up: where populated_kind_count scalar-projects populated_kinds on the tagged-union parent-level closed-set-inversion axis, distinct_kind_count scalar-projects distinct_kinds on the slice-level closed-set-inversion axis. The two primitives close the scalar-cardinality refinement at two adjacent typescape sites — one per closed-set-addressed slice-level refinement, one per closed-set-addressed tagged-union parent-level refinement — through the SAME ClosedSet::ALL-walk shape.

Compounding future consumers

• A future coherence check that enforces “every boundary carries at least ONE distinct kind” now reads slice.distinct_kind_count() > 0 at ONE call site rather than paying for slice.distinct_kinds().len() > 0 (with its intermediate heap allocation) or the eight-way sweep with has_kind at the callsite.
• A future require-tag classifier arm that surfaces the distinct-set cardinality as a scalar (a hypothetical condition-kinds-distinct-<n> prefix family named in Self::distinct_kinds’s doc-comment as a compounding-future consumer) reaches this ONE primitive without allocating.
• A future audit dump reporting “boundary carries N distinct kinds” reaches slice.distinct_kind_count() directly rather than restating the .iter().filter(...).count() closure body.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The scalar cardinality lives at ONE substrate site as a typed projection of Self::distinct_kinds onto its .len(), and the default body composes against Self::has_kind over the closed set ConditionKind::ALL byte-identically to distinct_kinds without the intermediate Vec. Every downstream aggregate consumer binds through the SAME shape rather than paying for the allocation to reach the cardinality.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically (the closed-set walk picks up the new entry) and every downstream consumer sees the wider cardinality without further per-caller edit.

fn missing_kinds(&self) -> Vec<ConditionKind>

The set of ConditionKind variants that do NOT appear in this slice, projected in ConditionKind::ALL order — the closed- set-inversion COMPLEMENT of Self::distinct_kinds. Default body: ConditionKind::ALL.into_iter().filter(|k| !self.has_kind(*k)).collect() — a thin projection over the closed set that composes against Self::has_kind per variant under a negated predicate.

Sibling to Self::distinct_kinds

Complement peer of the closed-set-inversion widened primitive on the slice-level presence-probe axis. Where distinct_kinds returns the SET of kinds that DO appear at least once, missing_kinds returns the SET of kinds that DO NOT appear. Both walk ConditionKind::ALL in canonical order and compose against the same Self::has_kind point probe. The two widened primitives PARTITION ConditionKind::ALL: their union equals ConditionKind::ALL, their intersection is empty, and their cardinalities sum to ConditionKind::ALL.len() — three composition laws pinned as the seventh, eighth, and ninth arms of the substrate testkit assert_slice_refinement_composition_laws.

Peer to crate::tagged_union::TaggedUnion::populated_kinds’s

hypothetical unpopulated_kinds complement

Same shape at the peer axis one struct layer up: fixing the parent-side carrier and inverting the presence probe over the closed set. The two primitives close the “closed-set complement” refinement at two adjacent typescape sites — one per closed-set- addressed slice-level refinement (this primitive), one per closed-set-addressed tagged-union parent-level refinement (a symmetric future addition).

Semantics — canonical subsequence of ConditionKind::ALL

Returns a Vec<ConditionKind> whose elements appear in ConditionKind::ALL order with no duplicates. An empty slice returns ConditionKind::ALL.to_vec() (every kind is missing). A slice that carries every variant returns an empty vec (no kind is missing). A slice that carries the same ConditionKind at multiple positions still contributes ZERO entries to the missing set at that kind (the closed-set complement is a SET operation — multiplicity on the present side is irrelevant to absence on the missing side).

Compounding future consumers

• A future coherence check that enforces “every process boundary carries a ConditionKind::JobAttested postcondition” now surfaces the operator-facing diagnostic spec.boundary.postconditions.missing_kinds() verbatim (naming EVERY kind absent from postconditions in canonical order) rather than reaching for !has_kind(JobAttested) at a per-kind callsite and paying to re-author the diagnostic list.
• An operator-facing “boundary is MISSING [JobAttested, ClosedLoopAuth]” audit dump reads boundary.postconditions.missing_kinds() directly at ONE call site rather than restating the negated closed-set walk at every consumer.
• A fleet-wide gap analysis (“which processes are missing a ClosedLoopAuth postcondition”) reaches this ONE primitive through spec.boundary.postconditions.missing_kinds() .contains(&ConditionKind::ClosedLoopAuth) rather than paying for the negated .has_kind sweep at every callsite.
• A hypothetical condition-kinds-missing-<n> require-tag classifier prefix family that publishes the missing-set cardinality as a scalar reads Self::missing_kind_count (the scalar-cardinality peer of this widened primitive) without allocating.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The closed-set complement lives at ONE substrate site as a typed projection of Self::has_kind over the closed set ConditionKind::ALL under negation. Every downstream gap- analysis consumer binds through the SAME shape rather than restating the negated ALL-filter closure body.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically (the closed-set walk picks up the new entry on the missing side WITHOUT further per-caller edit — any slice that doesn’t yet populate the new kind sees it listed as missing at every downstream callsite).

fn iter_missing_kinds(&self) -> impl Iterator<Item = ConditionKind> + '_

Zero-allocation iterator peer of Self::missing_kinds — walk ConditionKind::ALL in canonical order and yield every ConditionKind whose corresponding slot on this slice is EMPTY (no Condition in the slice carries that kind), WITHOUT materializing an intermediate Vec<ConditionKind>.

Default body: ConditionKind::ALL.iter().copied().filter(|&k| !self.has_kind(k)). The composition law missing_kinds() == iter_missing_kinds().collect::<Vec<_>>() holds by construction — Self::missing_kinds’s default body IS self.iter_missing_kinds().collect(), so a caller that overrides the widened Vec primitive with a divergent walk simultaneously drifts both surfaces (surfacing at the substrate testkit assert_slice_refinement_composition_laws which pins the Vec projection equals iter().collect()).

Sibling to Self::missing_kinds / Self::missing_kind_count

Load-bearing iterator peer of the slice-level closed-set-complement axis — where missing_kinds returns the SET (heap-allocated Vec, canonical ConditionKind::ALL order) and missing_kind_count scalar-projects its cardinality, iter_missing_kinds opens the walk as a Copy iterator so consumers that need a short- circuiting fold avoid the intermediate allocation entirely.

Peer to Self::iter_distinct_kinds

Closed-set-COMPLEMENT peer under a NEGATED point-probe. The two iterators PARTITION ConditionKind::ALL: iter_distinct_kinds().chain(iter_missing_kinds()).collect::<HashSet<_>>() equals ConditionKind::ALL.iter().copied().collect(), and the two iterators yield disjoint element sets.

Peer to crate::tagged_union::TaggedUnion::iter_missing_kinds

Same shape at the peer axis one struct layer up: where iter_missing_kinds on the tagged-union parent opens the closed- set-complement walk under a negated has point-probe, this method opens the SAME walk on the slice-level presence-probe axis under a negated has_kind point-probe. Both close the “load-bearing iterator on the complement side” refinement at two adjacent typescape sites through the SAME <CLOSED_SET>::ALL.iter().copied().filter(|&k| !has_probe(k)) composition body.

Compounding future consumers

• Every scalar closed-set-complement peer already at the trait (missing_kind_count, first_missing_kind, last_missing_kind, unique_missing_kind, is_kind_saturated, has_any_missing_kind, has_unique_missing_kind, has_multiple_missing_kinds, has_at_most_one_missing_kind) folds a specialization of ConditionKind::ALL.iter().filter(|k| !self.has_kind(**k)) — they can compose over iter_missing_kinds() at ONE substrate site rather than restating the closed-set walk body per peer.
• A downstream diagnostic composer (an operator-facing “still missing: [{}]” message that streams the label list into a write! buffer on the partially-populated arm) reads slice.iter_missing_kinds().map(|k| k.label()) and folds through itertools::join without the allocation Vec<ConditionKind> -> String pays.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The load-bearing iterator projection on the complement side lives at ONE substrate site, byte-for-byte symmetrical with Self::iter_distinct_kinds under a negated has_kind predicate.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches the walk mechanically (the closed-set filter picks up the new entry on the missing side) and every downstream fold sees the wider complement without further per-caller edit.

fn missing_kind_count(&self) -> usize

Scalar cardinality projection of Self::missing_kinds onto its .len() — the number of ConditionKind variants that do NOT appear in this slice. Default body: ConditionKind::ALL.iter().filter(|k| !self.has_kind(**k)).count() — a closed-set walk composed against Self::has_kind per variant under a NEGATED point-probe, WITHOUT materializing the intermediate Vec<ConditionKind> a caller reaching only for the scalar cardinality otherwise pays for. An empty slice returns ConditionKind::ALL.len() (every kind is missing); a slice carrying every variant returns 0 (no kind is missing).

Sibling to Self::missing_kinds / Self::distinct_kind_count

Scalar projection of the closed-set-complement widened primitive — where missing_kinds returns the SET (a Vec<ConditionKind> in canonical ConditionKind::ALL order), missing_kind_count collapses that set to its cardinality. The composition law missing_kind_count() == missing_kinds().len() binds the scalar projection to the widened primitive at the trait’s default body and is swept substrate-wide by assert_slice_refinement_composition_laws as its scalar- cardinality-complement arm.

Byte-for-byte peer of Self::distinct_kind_count one axis over (under a negated has_kind predicate): where distinct_kind_count scalar-projects the closed-set-INVERSION widened primitive distinct_kinds, this method scalar-projects the closed-set- COMPLEMENT widened primitive missing_kinds. The two scalar projections PARTITION the closed-set cardinality: distinct_kind_count() + missing_kind_count() == ConditionKind::ALL.len() — the scalar consequence of the (distinct_kinds, missing_kinds) partition law that assert_slice_refinement_composition_laws pins at the widened-primitive layer.

Peer to crate::tagged_union::TaggedUnion::populated_kind_count’s

hypothetical complement peer

Same shape at the peer axis one struct layer up: fixing the slice-side carrier and inverting the presence probe over the closed set under a negated predicate. The two primitives close the “closed-set-complement scalar cardinality” refinement at two adjacent typescape sites — one per closed-set-addressed slice-level refinement (this primitive), one per closed-set- addressed tagged-union parent-level refinement (a symmetric future addition).

Compounding future consumers

• A future coherence check that enforces “every process boundary carries EVERY ConditionKind under some slot” now reads spec.boundary.postconditions.missing_kind_count() == 0 at ONE call site rather than paying for spec.boundary.postconditions.missing_kinds().is_empty() (with its intermediate heap allocation) or the eight-way negated sweep with has_kind at the callsite.
• A future require-tag classifier arm that surfaces the missing- set cardinality as a scalar (the exact condition-kinds-missing-<n> require-tag classifier prefix family called out in Self::missing_kinds’s doc-comment as a hypothetical compounding-future consumer) reaches this ONE primitive without allocating.
• A future gap-analysis dashboard reporting “boundary is missing N of {N_TOTAL} distinct kinds” reaches slice.missing_kind_count() directly rather than restating the negated .iter().filter(...).count() closure body.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The scalar cardinality lives at ONE substrate site as a typed projection of Self::missing_kinds onto its .len(), and the default body composes against Self::has_kind over the closed set ConditionKind::ALL under negation byte- identically to missing_kinds without the intermediate Vec. Every downstream aggregate consumer binds through the SAME shape rather than paying for the allocation to reach the cardinality.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically (the closed-set walk picks up the new entry on the missing side WITHOUT further per-caller edit — any slice that doesn’t yet populate the new kind sees the cardinality rise by one at every downstream callsite).

fn first_distinct_kind(&self) -> Option<ConditionKind>

Short-circuiting Option<ConditionKind> peer of Self::distinct_kinds — the FIRST ConditionKind variant present in this slice, in canonical ConditionKind::ALL order, or None when the slice carries no matching kind. Default body: ConditionKind::ALL.iter().copied().find(|k| self.has_kind(*k)) — a closed-set walk composed against Self::has_kind per variant that SHORT-CIRCUITS at the earliest match.

Sibling to Self::distinct_kinds / Self::distinct_kind_count

Third refinement on the closed-set-inversion axis, Option<ConditionKind>- valued: distinct_kinds returns the SET, distinct_kind_count scalar-projects the cardinality, and first_distinct_kind scalar-projects the SET onto its earliest element. The composition law first_distinct_kind() == distinct_kinds().first().copied() binds the earliest-element projection to the widened primitive at the trait’s default body — pinned substrate-wide by assert_slice_refinement_composition_laws as its earliest-element-inversion arm. Both coarser projections agree on emptiness: first_distinct_kind().is_none() == (distinct_kind_count() == 0).

Peer to crate::tagged_union::TaggedUnion::first_populated_kind

Same shape at the peer axis one struct layer up: fixing the carrier and short-circuiting on the earliest ConditionKind::ALL hit under Self::has_kind. TaggedUnion::first_populated_kind walks the tagged-union parent’s closed set; first_distinct_kind here walks ConditionKind::ALL on the slice-level presence-probe axis. The two primitives close the “earliest-element scalar- projection of the closed-set-inversion widened primitive” refinement at two adjacent typescape sites — one per closed-set- addressed slice-level refinement (this primitive), one per closed- set-addressed tagged-union parent-level refinement.

Semantics

Returns Some(k) where k is the earliest ConditionKind::ALL entry with self.has_kind(k) == true, or None when no kind is present. An empty slice returns None. A slice carrying multiple variants returns the earliest one in ConditionKind::ALL order — a strictly more informative projection than distinct_kinds().first().copied() without materializing the intermediate Vec<ConditionKind> the widened primitive otherwise pays for.

Compounding future consumers

• An operator-facing “first present kind” diagnostic on an audit dump that names ONE kind rather than the full set reaches this ONE substrate site rather than paying for slice.distinct_kinds().first().copied() (with its intermediate heap allocation).
• A first-distinct-<kind> require-tag classifier arm reads this primitive with no allocation, byte-for-byte symmetrical with slice.has_kind(kind) under a closed-set-inversion projection.
• A fast-path branch that discriminates “empty” from “any populated” reads slice.first_distinct_kind().is_some() at ONE call site rather than allocating a Vec<ConditionKind> through !distinct_kinds().is_empty() or paying for the full distinct_kind_count() > 0 walk.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The earliest-element projection lives at ONE substrate site as a typed projection of Self::has_kind over the closed set ConditionKind::ALL under short-circuit walk semantics.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically (the closed-set walk picks up the new entry) — every downstream consumer sees the wider earliest-hit projection without further per-caller edit.

fn first_missing_kind(&self) -> Option<ConditionKind>

Short-circuiting Option<ConditionKind> peer of Self::missing_kinds — the FIRST ConditionKind variant ABSENT from this slice, in canonical ConditionKind::ALL order, or None when the slice carries every variant. Default body: ConditionKind::ALL.iter().copied().find(|k| !self.has_kind(*k)) — a closed-set walk composed against Self::has_kind per variant under NEGATION with SHORT-CIRCUIT at the earliest empty slot.

Sibling to Self::missing_kinds / Self::missing_kind_count

Third refinement on the closed-set-complement axis, Option<ConditionKind>-valued: missing_kinds returns the SET, missing_kind_count scalar-projects the cardinality, and first_missing_kind scalar-projects the SET onto its earliest element. The composition law first_missing_kind() == missing_kinds().first().copied() binds the earliest-element projection to the widened primitive at the trait’s default body — pinned substrate-wide by assert_slice_refinement_composition_laws as its earliest-element-complement arm. Both coarser projections agree on saturation: first_missing_kind().is_none() == (missing_kind_count() == 0).

Peer to Self::first_distinct_kind

Closed-set-complement peer of the closed-set-inversion earliest- element primitive under a negated has_kind predicate. The two primitives PARTITION ConditionKind::ALL’s earliest-element projection: at least one of first_distinct_kind() and first_missing_kind() is Some on any non-degenerate closed set (both are Some iff 1 ≤ distinct_kind_count() < ConditionKind::ALL.len(); only the distinct-side is Some on a saturated slice; only the missing-side is Some on an empty slice).

Peer to crate::tagged_union::TaggedUnion::first_missing_kind

Same shape at the peer axis one struct layer up under a negated predicate. The two primitives close the “earliest-element scalar- projection of the closed-set-complement widened primitive” refinement at two adjacent typescape sites — one per closed-set- addressed slice-level refinement (this primitive), one per closed- set-addressed tagged-union parent-level refinement.

Semantics

An empty slice returns Some(ConditionKind::ALL[0]) (every kind missing, first hit is index 0). A slice populating exactly k returns Some(ConditionKind::ALL[0]) if k != ALL[0], else Some(ALL[1]) (the earliest non-k entry). A saturated slice carrying every variant returns None.

Compounding future consumers

• An operator-facing “first still-unfilled kind” diagnostic on a partially-populated boundary reads boundary.postconditions.first_missing_kind() at ONE substrate site — a strictly-more-informative projection than !has_kind(JobAttested) at a per-kind callsite for a fleet-wide “which processes are missing at least one closed-loop kind” audit.
• A first-missing-<kind> require-tag classifier arm reads this primitive with no allocation, byte-for-byte symmetrical with slice.first_distinct_kind().
• A fast-path branch that discriminates “saturated” from “at least one missing” reads slice.first_missing_kind().is_some() at ONE call site rather than allocating through !missing_kinds().is_empty() or paying for the full missing_kind_count() > 0 walk.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The complement-earliest-element projection lives at ONE substrate site as a typed projection of Self::has_kind over the closed set ConditionKind::ALL under negation with short- circuit walk semantics.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically (the closed-set walk picks up the new entry on the missing side) — every downstream consumer sees the wider complement’s earliest hit without further per-caller edit.

fn last_distinct_kind(&self) -> Option<ConditionKind>

Short-circuiting Option<ConditionKind> peer of Self::distinct_kinds — the LAST ConditionKind variant present in this slice, in canonical ConditionKind::ALL order, or None when the slice carries no variant. Default body: ConditionKind::ALL.iter().rev().copied().find(|k| self.has_kind(*k)) — a REVERSED closed-set walk composed against Self::has_kind per variant that SHORT-CIRCUITS at the latest hit.

Sibling to Self::distinct_kinds /

Self::distinct_kind_count / Self::first_distinct_kind

Fourth refinement on the closed-set-inversion axis and second scalar Option<ConditionKind> projection: distinct_kinds returns the SET, distinct_kind_count scalar-projects the cardinality, first_distinct_kind scalar-projects the SET onto its earliest element, and last_distinct_kind scalar- projects the SET onto its latest element. The composition law last_distinct_kind() == distinct_kinds().last().copied() binds the latest-element projection to the widened primitive at the trait’s default body — pinned substrate-wide by assert_slice_refinement_composition_laws as its latest-element-inversion arm. Both scalar projections agree on emptiness: last_distinct_kind().is_none() == first_distinct_kind().is_none() == distinct_kinds().is_empty().

Peer to Self::first_distinct_kind

Time-reversed peer under the SAME has_kind predicate: where first_distinct_kind walks ConditionKind::ALL forward and SHORT-CIRCUITS at the earliest hit, this primitive walks the SAME closed set in reverse and SHORT-CIRCUITS at the latest hit. The two primitives close the “endpoint scalar-projection of the closed-set-inversion widened primitive” refinement pair at one substrate site — one per endpoint. On a slice with exactly one distinct kind both projections agree; on a slice with distinct-kind-count ≥ 2 they yield distinct results (the earliest and latest elements of the closed-set-inversion respectively).

Semantics

An empty slice returns None (no kind present, no hit on any walk direction). A slice populating exactly k returns Some(k) (single hit; earliest = latest). A saturated slice carrying every variant returns Some(ConditionKind::ALL.last() .unwrap()) (the last ALL entry hits at the earliest walk step of the reversed walk).

Compounding future consumers

• A last-distinct-<kind> require-tag classifier arm reads the latest-populated kind through this ONE substrate primitive with no allocation, byte-for-byte symmetrical with the earliest-hit slice.first_distinct_kind() peer.
• A future coherence check that surfaces “boundary ends with ClosedLoopAuth” reads spec.boundary.postconditions.last_distinct_kind() == Some(ConditionKind::ClosedLoopAuth) at ONE call site rather than paying for spec.boundary.postconditions .distinct_kinds().last() == Some(&…) with its intermediate heap allocation.
• Combined with Self::first_distinct_kind, operator diagnostics that render a “populated-kind range” summary (first..=last on the closed-set-inversion projection) read the two endpoints through TWO substrate primitives at symmetric shapes without allocating.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The latest-element projection lives at ONE substrate site as a typed projection of Self::has_kind over the closed set ConditionKind::ALL under REVERSED short-circuit walk semantics; byte-for-byte peer of the earliest-element projection under FORWARD walk semantics.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically (the reversed closed-set walk picks up the new entry at the appropriate position) — every downstream consumer sees the wider latest-hit projection without further per-caller edit.

fn last_missing_kind(&self) -> Option<ConditionKind>

Short-circuiting Option<ConditionKind> peer of Self::missing_kinds — the LAST ConditionKind variant ABSENT from this slice, in canonical ConditionKind::ALL order, or None when the slice carries every variant. Default body: ConditionKind::ALL.iter().rev().copied().find(|k| !self.has_kind(*k)) — a REVERSED closed-set walk composed against Self::has_kind per variant under NEGATION with SHORT-CIRCUIT at the latest empty slot.

Sibling to Self::missing_kinds /

Self::missing_kind_count / Self::first_missing_kind

Fourth refinement on the closed-set-complement axis and second scalar Option<ConditionKind> projection: missing_kinds returns the SET, missing_kind_count scalar-projects the cardinality, first_missing_kind scalar-projects the SET onto its earliest element, and last_missing_kind scalar-projects the SET onto its latest element. The composition law last_missing_kind() == missing_kinds().last().copied() binds the latest-element projection to the widened primitive at the trait’s default body — pinned substrate-wide by assert_slice_refinement_composition_laws as its latest-element-complement arm. Both scalar projections agree on saturation: last_missing_kind().is_none() == first_missing_kind().is_none() == missing_kinds().is_empty().

Peer to Self::first_missing_kind

Time-reversed peer under the SAME negated has_kind predicate: where first_missing_kind walks ConditionKind::ALL forward under negation and SHORT-CIRCUITS at the earliest empty slot, this primitive walks the SAME closed set in reverse and SHORT- CIRCUITS at the latest empty slot. The two primitives close the “endpoint scalar-projection of the closed-set-complement widened primitive” refinement pair at one substrate site.

Peer to Self::last_distinct_kind

Closed-set-complement peer of the closed-set-inversion latest- element primitive under a NEGATED has_kind predicate. Along with Self::first_distinct_kind and Self::first_missing_kind the four scalar-endpoint projections partition the endpoint axis into (present, absent) × (earliest, latest) — every endpoint-addressable coherence check reads ONE of the four at ONE call site, never the full Vec<ConditionKind> walk.

Semantics

An empty slice returns Some(ConditionKind::ALL.last().unwrap()) (every kind missing, latest hit is the last ALL entry). A slice populating exactly k returns Some(ALL.last().unwrap()) if k != ALL.last().unwrap(), else Some(ALL[ALL.len() - 2]) (the latest non-k entry). A saturated slice carrying every variant returns None.

Compounding future consumers

• An operator-facing “last still-unfilled kind” diagnostic on a partially-populated boundary reads boundary.postconditions.last_missing_kind() at ONE substrate site — a strictly-more-informative projection than !has_kind(ClosedLoopAuth) at a per-kind callsite for a fleet-wide “which processes are latest-missing a specific closed-loop kind” audit.
• A last-missing-<kind> require-tag classifier arm reads this primitive with no allocation, byte-for-byte symmetrical with the earliest-hit slice.first_missing_kind() peer.
• Combined with Self::first_missing_kind, a coherence check that renders a “missing-kind range” summary reads the two endpoints through TWO substrate primitives at symmetric shapes without allocating through missing_kinds().

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The complement-latest-element projection lives at ONE substrate site as a typed projection of Self::has_kind over the closed set ConditionKind::ALL under negation with REVERSED short-circuit walk semantics; byte-for-byte peer of the complement-earliest-element projection under FORWARD walk semantics.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically (the reversed closed-set walk picks up the new entry on the missing side at the appropriate position) — every downstream consumer sees the wider complement’s latest hit without further per-caller edit.

fn is_kind_saturated(&self) -> bool

Boolean saturation predicate on the closed-set-inversion axis — true iff EVERY ConditionKind::ALL variant appears at least once in this slice (equivalently, Self::missing_kinds is empty).

Default body: ConditionKind::ALL.iter().all(|k| self.has_kind(*k)) — a SHORT-CIRCUITING closed-set walk composed against Self::has_kind per variant that returns false at the FIRST missing kind, WITHOUT materializing Self::missing_kinds’s Vec and WITHOUT walking every entry to build Self::missing_kind_count’s scalar. Strictly cheaper than either widened primitive on every partially-populated arm (returns at the first empty slot rather than sweeping the full closed set).

Peer to crate::tagged_union::TaggedUnion::is_saturated

Slice-level peer of the tagged-union parent-level saturation predicate one struct-layer up: where is_saturated names the tagged-union arm where every <Self::Kind as ClosedSet>::ALL slot is populated, is_kind_saturated names the slice arm where every ConditionKind::ALL variant appears at least once. Both short-circuit at the first missing entry under the SAME <CLOSED_SET>::ALL.iter().all(has) walk shape at two adjacent typescape sites.

Sibling to Self::missing_kind_count / Self::missing_kinds

Boolean cardinality-endpoint peer of the scalar cardinality primitive on the closed-set-complement axis — where missing_kind_count returns the FULL scalar (any usize in 0..=ConditionKind::ALL.len()), is_kind_saturated collapses that scalar to its zero-arm Boolean projection. The composition law is_kind_saturated() == (missing_kind_count() == 0) binds the Boolean projection to the scalar primitive at the trait’s default body — swept substrate-wide by assert_slice_refinement_composition_laws as its saturation-endpoint arm.

Semantics

An empty slice returns false (no kind is populated). A slice carrying a strict subset of ConditionKind::ALL returns false. A slice that carries every variant at least once (multiplicity is irrelevant) returns true — the SOLE arm where is_kind_saturated returns true.

Compounding future consumers

• A future coherence check that enforces “every process boundary exhaustively covers every ConditionKind” reads boundary.postconditions.is_kind_saturated() at ONE call site — one short-circuit walk, no allocation, no scalar equality comparison against ConditionKind::ALL.len().
• An is-kind-saturated require-tag classifier arm reaches this primitive with no allocation, byte-for-byte peer of the tagged-union is-saturated classifier one struct-layer up.
• A fleet-wide gap-analysis dashboard fast-path that discriminates “boundary spans every kind” from “boundary is missing some kind” reads boundary.postconditions.is_kind_saturated() at ONE call site rather than restating either boundary.postconditions.missing_kind_count() == 0 (which walks every slot to count) or boundary.postconditions.missing_kinds().is_empty() (which allocates the Vec before the emptiness check).

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The saturation-endpoint projection lives at ONE substrate site as a typed short-circuiting closed-set walk ConditionKind::ALL.iter().all(has_kind). Every downstream consumer binds through the SAME shape rather than restating the == ConditionKind::ALL.len() scalar composition body.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the all short-circuit — a slice that was previously saturated is no longer saturated at every downstream callsite unless it also carries the new variant.

fn is_kind_empty(&self) -> bool

Boolean cardinality zero-endpoint peer of Self::is_kind_saturated on the closed-set-inversion axis — true iff NO ConditionKind::ALL variant appears in this slice (equivalently, Self::distinct_kinds is empty, Self::distinct_kind_count == 0, and Self::first_distinct_kind is None).

Default body: self.iter_distinct_kinds().next().is_none() — a SHORT-CIRCUITING closed-set walk composed against the load-bearing distinct iterator that returns true iff the first hit is None, WITHOUT materializing Self::distinct_kinds’s Vec, WITHOUT walking every slot to build Self::distinct_kind_count’s scalar, and WITHOUT allocating the closed-set-inversion scan. Strictly cheaper than either widened primitive on every arm because the walk short-circuits at the first present kind on the has-side walk rather than paying for the Vec allocation or the full cardinality count.

Peer to crate::tagged_union::TaggedUnion::is_empty

Slice-level peer of the tagged-union parent-level zero-endpoint predicate one struct-layer up: where crate::tagged_union::TaggedUnion::is_empty answers “is EVERY slot on the tagged-union parent empty?”, is_kind_empty answers “does NO kind appear in ANY condition of the slice?”. Both short-circuit at the first present entry under the SAME <CLOSED_SET>::ALL.iter().any(has)-then-negate walk shape at two adjacent typescape sites — the two primitives close the zero- endpoint on the closed-set-inversion axis at both struct layers under the SAME shape.

Sibling to Self::is_kind_saturated

Axis-parity mirror of the closed-set-complement saturation- endpoint primitive on the closed-set-inversion axis — where is_kind_saturated returns true iff missing_kind_count == 0 (every kind PRESENT), is_kind_empty returns true iff distinct_kind_count == 0 (every kind ABSENT). Together the two Booleans name the (empty, saturated) endpoints of the (distinct, missing) partition: a slice is EMPTY iff is_kind_empty() returns true (equivalently, is_kind_saturated == false AND no partial-populated arm applies); a slice is SATURATED iff is_kind_saturated() returns true. On any N ≥ 1 closed set, at most ONE of the two returns true; on N == 0 closed sets both return true vacuously. Byte-for-byte peer of the tagged-union is_empty / is_saturated sibling pair one struct-layer up.

Sibling to Self::has_any_distinct_kind

Boolean zero-endpoint peer of the at-least-one halfspace primitive on the closed-set-inversion axis — where has_any_distinct_kind returns true iff at least one kind is PRESENT, is_kind_empty returns its Boolean-negation: true iff distinct_kind_count == 0. Together the two Booleans partition the distinct-cardinality closed set: exactly one of is_kind_empty() and has_any_distinct_kind() is true for every slice. The definitional negation law is_kind_empty() == !has_any_distinct_kind() is pinned as a first-class typed invariant by assert_slice_refinement_composition_laws as its zero-endpoint arm on the distinct axis, byte-for-byte peer of the missing-axis pin has_any_missing_kind() == !is_kind_saturated().

Sibling to Self::distinct_kinds / Self::distinct_kind_count

Boolean zero-endpoint peer of the widened + scalar closed-set- inversion primitives — where distinct_kinds returns the FULL distinct SET and distinct_kind_count returns its cardinality, is_kind_empty collapses either the widened primitive to its emptiness Boolean or the scalar to its == 0 cardinality-endpoint Boolean. The composition laws is_kind_empty() == distinct_kinds().is_empty() and is_kind_empty() == (distinct_kind_count() == 0) bind this Boolean projection to the widened + scalar primitives at the trait’s default body — strictly cheaper than either widened primitive on every non-empty arm because the walk short-circuits at the first present kind rather than allocating the closed-set- inversion scan or walking every slot to build the scalar cardinality.

Semantics

An empty slice returns true — the SOLE arm where is_kind_empty returns true on any N ≥ 1 closed set, byte-for-byte peer of the SOLE arm where is_kind_saturated returns true (a slice carrying every variant at least once). A slice carrying a strict subset of ConditionKind::ALL returns false. A saturated slice returns false on N ≥ 1 closed sets. Multiplicity is irrelevant on both sides — the predicate collapses to the distinct-set’s emptiness.

Compounding future consumers

• A fleet-wide “no coverage at all” fast-path that discriminates “the slice is empty” from “the slice carries at least one kind” reads boundary.postconditions.is_kind_empty() at ONE call site rather than restating distinct_kind_count() == 0 (which walks every slot to count), distinct_kinds().is_empty() (which allocates the Vec before the emptiness check), or negating has_any_distinct_kind() at the callsite.
• An is-kind-empty require-tag classifier arm reaches this primitive with no allocation, byte-for-byte peer of the tagged-union is-empty classifier one struct-layer up under the SAME zero-endpoint short-circuit shape.
• A coherence check that flags “any process boundary whose postcondition slice is empty” reads boundary.postconditions.is_kind_empty() at ONE substrate primitive per test rather than restating the emptiness body at every callsite.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The zero-endpoint projection on the closed-set-inversion axis lives at ONE substrate site as a short-circuiting closed-set walk over the load-bearing distinct iterator. Every downstream consumer whose semantic reading is “no kind is present” reads through this primitive rather than paying for the widened primitive’s Vec allocation, the scalar counter’s full-slot walk, or the negation-at-callsite of the at-least-one halfspace primitive.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the load-bearing distinct iterator — an empty slice (returning true here) that later picks up any variant flips to false at every downstream is-kind-empty callsite. Byte-for-byte symmetrical with the wider-set propagation on is_kind_saturated under the (distinct, missing) axis-parity.

fn is_kind_partially_covered(&self) -> bool

Boolean cardinality parent-state middle-arm peer of Self::is_kind_empty and Self::is_kind_saturated on the closed-set-partition axis — true iff AT LEAST ONE ConditionKind::ALL variant appears at least once in this slice AND AT LEAST ONE ConditionKind::ALL variant is absent from every condition (equivalently, 0 < distinct_kind_count < ConditionKind::ALL.len() and 0 < missing_kind_count < ConditionKind::ALL.len()).

Default body: a FUSED short-circuit closed-set walk over ConditionKind::ALL that flips a two-bit (has_present, has_missing) witness on each kind under Self::has_kind and returns true at the FIRST kind whose flip closes both bits, WITHOUT materializing Self::distinct_kinds or Self::missing_kinds, WITHOUT walking every slot to build Self::distinct_kind_count or Self::missing_kind_count, and WITHOUT allocating a two-Vec negation-of-both-endpoints composition at the callsite. Byte-for-byte cheaper than the widened negation composition !self.is_kind_empty() && !self.is_kind_saturated() (which pays two separate ALL-length short-circuit walks on saturated / empty arms) on every arm where the FIRST and SECOND slot kinds bracket the closed set on opposite bits — the fused walk exits on the SECOND slot of ConditionKind::ALL whenever the two pass-side bits close, cheaper than either widened primitive on the mid-arm sweep.

Peer to crate::tagged_union::TaggedUnion::is_partially_populated

Slice-level peer of the tagged-union parent-level middle-arm predicate one struct-layer up: where crate::tagged_union::TaggedUnion::is_partially_populated answers “is SOME slot on the tagged-union parent occupied AND SOME slot missing?”, is_kind_partially_covered answers “does SOME kind appear in AT LEAST ONE condition of the slice AND SOME kind APPEAR IN NONE?”. Both compose against a FUSED short-circuit closed-set walk under the SAME presence predicate (has(kind) / has_kind(kind)) at two adjacent typescape sites — the two primitives close the parent-state middle-arm on the closed-set partition at both struct layers under the SAME shape. The trichotomy partition law usize::from(is_kind_empty()) + usize::from(is_kind_partially_covered()) + usize::from(is_kind_saturated()) == 1 on any N ≥ 1 closed set is pinned as a first-class typed invariant by assert_slice_refinement_composition_laws as its parent-state trichotomy arm, byte-for-byte peer of crate::tagged_union::assert_is_partially_populated_matches_cardinality one struct-layer up.

Sibling to Self::is_kind_empty / Self::is_kind_saturated

Third and final arm of the (empty, partially covered, saturated) parent-state trichotomy on the closed-set-partition axis at the slice level, closing the natural partition alongside is_kind_empty (=0 zero-endpoint on the distinct axis) and is_kind_saturated (=0 zero-endpoint on the missing axis). Every slice satisfies EXACTLY ONE of the three Boolean projections on any N ≥ 1 closed set — the three primitives partition the (distinct_kind_count, missing_kind_count) product at (0, N), (open interval, open interval), and (N, 0) respectively.

Composition laws

• is_kind_partially_covered() == !is_kind_empty() && !is_kind_saturated() — the negation-of-both-endpoints composition, at the trait default body’s SAME fused short-circuit walk.
• is_kind_partially_covered() == has_any_distinct_kind() && has_any_missing_kind() — the paired at-least-one-halfspace composition binding this Boolean projection to the at-least-one halfspace peers on both axes.
• is_kind_partially_covered() == (distinct_kind_count() > 0 && missing_kind_count() > 0) — the paired scalar-projection composition binding this Boolean projection to the widened + scalar peers on both axes.

Semantics

An empty slice returns false (0 distinct + N missing hits the is_kind_empty arm, not the middle arm). A slice carrying a strict subset of ConditionKind::ALL returns true on any N ≥ 2 closed set (some kind present, some absent). A saturated slice returns false (N distinct + 0 missing hits the is_kind_saturated arm, not the middle arm). Multiplicity is irrelevant on both sides — the predicate collapses to non-emptiness of both the distinct SET and the missing SET.

Compounding future consumers

• A boundary-progress “some kinds covered, some pending” diagnostic on a Boundary slice reads boundary.postconditions.is_kind_partially_covered() at ONE substrate site — the exact “in-flight coverage” arm — rather than composing !boundary.postconditions.is_kind_empty() && !boundary.postconditions.is_kind_saturated() (two closed-set walks) or boundary.postconditions.distinct_kind_count() > 0 && boundary.postconditions.missing_kind_count() > 0 (two counter walks with no short-circuit).
• A fleet-wide “mixed coverage” fast-path that discriminates “partial” from “empty or saturated” reads this primitive with ONE fused short-circuit walk, strictly cheaper than either widened composition.
• An is-kind-partially-covered require-tag classifier arm reaches this primitive at ONE call site, byte-for-byte symmetrical with the sibling is-kind-empty / is-kind-saturated arms on the closed parent-state trichotomy.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The parent-state middle-arm projection on the closed-set partition lives at ONE substrate site as a FUSED short-circuit walk over ConditionKind::ALL under Self::has_kind with early exit on the first observed present/missing pair — byte-for-byte cheaper than the widened negation-of-both- endpoints composition, and semantically identical on every arm. The trichotomy partition law is_kind_empty + is_kind_partially_covered + is_kind_saturated == 1 lives at ONE substrate site inside the composition-law testkit’s per-arm sweep — pinned across every production slice at compile time via the trait’s default body composition, not per-slice.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the fused walk — the trichotomy holds on the widened kind set without further per-caller edit (a slice previously at the middle arm continues to satisfy it if it does not add the new variant; a previously-saturated slice that leaves the new variant missing becomes partially covered at every downstream callsite).

fn has_any_distinct_kind(&self) -> bool

Boolean at-least-one halfspace peer of Self::has_any_missing_kind on the closed-set-inversion axis — true iff AT LEAST ONE ConditionKind::ALL variant appears at least once in this slice (equivalently, Self::distinct_kinds is non-empty, Self::distinct_kind_count > 0, and Self::first_distinct_kind is Some).

Default body: ConditionKind::ALL.iter().copied().any(|k| self.has_kind(k)) — a SHORT-CIRCUITING closed-set walk that returns true at the FIRST populated kind WITHOUT materializing Self::distinct_kinds’s Vec, WITHOUT walking every slot to build Self::distinct_kind_count’s scalar, and WITHOUT allocating the closed-set-inversion scan. Strictly cheaper than either widened primitive on every non-empty arm because the walk short-circuits at the first has_kind hit rather than paying for the Vec allocation or the full cardinality count.

Peer to crate::tagged_union::TaggedUnion::has_any_populated_kind

Slice-level peer of the tagged-union parent-level at-least-one halfspace predicate one struct-layer up: where crate::tagged_union::TaggedUnion::has_any_populated_kind answers “is ANY slot on the tagged-union parent occupied?”, has_any_distinct_kind answers “does ANY kind appear in AT LEAST ONE condition of the slice?”. Both compose against a SHORT-CIRCUITING closed-set walk under the SAME has / has_kind predicate at two adjacent typescape sites — the two primitives close the at-least-one halfspace on the closed-set- inversion axis at both struct layers under the SAME shape.

Sibling to Self::has_any_missing_kind

Closed-set-inversion peer of the at-least-one halfspace on the closed-set-complement axis — where has_any_missing_kind returns true iff at least one kind is ABSENT, has_any_distinct_kind returns true iff at least one kind is PRESENT. Together with their zero-arm endpoints (Self::is_kind_saturated on the missing axis and the empty- slice endpoint on the distinct axis), the two Booleans partition the (distinct, missing) product: a slice is EMPTY iff neither has_any_distinct_kind() nor is_kind_saturated() returns true; a slice is SATURATED iff both has_any_distinct_kind() returns true and has_any_missing_kind() returns false; a slice is PARTIALLY POPULATED iff both has_any_distinct_kind() and has_any_missing_kind() return true.

Sibling to Self::distinct_kinds / Self::distinct_kind_count

Boolean at-least-one halfspace peer of the widened + scalar closed-set-inversion primitives — where distinct_kinds returns the FULL distinct SET and distinct_kind_count returns its cardinality, has_any_distinct_kind collapses either the widened primitive to its non-emptiness Boolean or the scalar to its >= 1 halfspace Boolean. The composition laws has_any_distinct_kind() == !distinct_kinds().is_empty() and has_any_distinct_kind() == (distinct_kind_count() > 0) bind this Boolean projection to the widened + scalar primitives at the trait’s default body — strictly cheaper than either widened primitive on every non-empty arm because the walk short-circuits at the first populated kind on the has-side walk rather than allocating the closed-set-inversion scan or walking every slot to build the scalar cardinality.

Semantics

An empty slice returns false — the SOLE arm on which has_any_distinct_kind returns false. A slice carrying any ConditionKind at least once returns true (a single- populated slice, a partially-populated slice, and a saturated slice all return true).

Compounding future consumers

• A fleet-wide “any coverage at all” fast-path that discriminates “the slice carries at least one closed-set kind” from “the slice is empty” reads boundary.postconditions.has_any_distinct_kind() at ONE call site rather than restating distinct_kind_count() > 0 (which walks every slot to count) or !distinct_kinds().is_empty() (which allocates the Vec before the negated emptiness check).
• A has-any-distinct-kind require-tag classifier arm reaches this primitive with no allocation, byte-for-byte peer of the tagged-union has-any-populated-kind classifier one struct- layer up under the SAME any(has) short-circuit shape.
• A coherence check that flags “any process boundary whose postcondition slice covers at least one ConditionKind” reads boundary.postconditions.has_any_distinct_kind() at ONE substrate primitive per test rather than restating the .iter().copied().any(|k| slice.has_kind(k)) body at every callsite.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The at-least-one halfspace projection on the closed-set- inversion axis lives at ONE substrate site as a typed short- circuiting closed-set walk ConditionKind::ALL.iter().any( has_kind). Every downstream consumer whose semantic reading is “at least one kind is present” reads through this primitive rather than paying for the widened primitive’s Vec allocation.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the any short-circuit — an empty slice (returning false here) that later picks up the new variant returns true at every downstream has-any- distinct-kind callsite.

fn has_unique_distinct_kind(&self) -> bool

Boolean cardinality-mid-endpoint peer of Self::has_any_distinct_kind on the closed-set-inversion axis — true iff EXACTLY ONE ConditionKind::ALL variant appears at least once in this slice (equivalently, Self::distinct_kind_count == 1, Self::distinct_kinds.len() == 1, and Self::first_distinct_kind equals Self::last_distinct_kind and is Some).

Default body: a two-step-short-circuit closed-set walk over Self::iter_distinct_kinds — pulls up to two hits off the load-bearing distinct iterator; the primitive returns true iff the first hit is Some and the second is None, WITHOUT materializing Self::distinct_kinds’s Vec and WITHOUT walking every slot to build Self::distinct_kind_count’s scalar. Short-circuits at the second distinct kind — strictly cheaper than either widened primitive on every arm with ≥ 2 distinct kinds.

Peer to crate::tagged_union::TaggedUnion::has_unique_populated_kind

Slice-level peer of the tagged-union parent-level cardinality-mid-endpoint predicate one struct-layer up: where crate::tagged_union::TaggedUnion::has_unique_populated_kind answers “is EXACTLY ONE slot on the tagged-union parent occupied?”, has_unique_distinct_kind answers “does EXACTLY ONE kind appear in AT LEAST ONE condition of the slice?”. Both compose against a two-step-short-circuit walk under the SAME presence predicate (has(kind) / has_kind(kind)) at two adjacent typescape sites — the two primitives close the exactly-one-arm on the closed-set-inversion axis at both struct layers under the SAME shape.

Sibling to Self::has_unique_missing_kind

Closed-set-inversion peer of the cardinality-mid-endpoint on the closed-set-complement axis — where has_unique_missing_kind returns true iff exactly one kind is ABSENT (the near-saturation-endpoint arm), has_unique_distinct_kind returns true iff exactly one kind is PRESENT (the singleton-coverage arm). Both close the exactly-one arm on their respective axis under the SAME two-step short-circuit walk shape via the load-bearing iterator peer.

Semantics

An empty slice returns false (0 distinct, not 1). A slice carrying a single ConditionKind (with any multiplicity) returns true — the SOLE arm where has_unique_distinct_kind returns true on any N ≥ 2 closed set. A slice carrying K ≥ 2 distinct kinds returns false. A saturated slice returns false on N ≥ 2 closed sets (every kind present, not exactly 1).

Compounding future consumers

• A fleet-wide “singleton coverage” fast-path that discriminates “the slice carries exactly one ALL variant” from every other cardinality reads boundary.postconditions.has_unique_distinct_kind() at ONE call site — one two-step short-circuit walk, no allocation, no scalar equality against 1, byte-for-byte peer of the tagged-union has-unique-populated-kind classifier one struct-layer up under the SAME two-step short-circuit shape.
• A has-unique-distinct-kind require-tag classifier arm reaches this primitive with no allocation.
• A future singleton-coverage diagnostic that prints “the SOLE ConditionKind covered by this Boundary” pairs has_unique_distinct_kind() with Self::first_distinct_kind to name the SOLE distinct kind without allocating Self::distinct_kinds’s Vec.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The cardinality-mid-endpoint projection on the closed-set- inversion axis lives at ONE substrate site as a typed two-step-short-circuit fold through the load-bearing Self::iter_distinct_kinds iterator — byte-for-byte peer of distinct_kind_count() composed against == 1, but with a second-distinct-slot short-circuit that the scalar counter primitive does not offer.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the short-circuit walk — a slice previously at the singleton-coverage arm (returned true here) that also picks up the new variant now has TWO distinct kinds and returns false.

fn unique_distinct_kind(&self) -> Option<ConditionKind>

Witnessing Option<ConditionKind> peer of Self::has_unique_distinct_kind on the closed-set-inversion axis — Some(k) iff k is the SOLE ConditionKind::ALL variant appearing at least once in this slice, else None.

Default body: a two-step-short-circuit fold through Self::iter_distinct_kinds — pull the first hit; return Some(first) iff the second hit is None, else None. Byte-for-byte peer of crate::tagged_union::TaggedUnion::unique_populated_kind one struct-layer up under the SAME iter_populated_kinds two-step short-circuit shape, and the WITNESSING scalar peer of the Boolean Self::has_unique_distinct_kind predicate at the SAME two-step short-circuit shape.

Sibling to Self::first_distinct_kind / Self::last_distinct_kind

FIFTH refinement on the closed-set-inversion axis under exactly- one-hit semantics, Option<ConditionKind>-valued: together with Self::first_distinct_kind and Self::last_distinct_kind the three primitives project Self::distinct_kinds onto its cardinality-conditioned scalar identity on the present side. The composition laws unique_distinct_kind().is_some() == (distinct_kind_count() == 1) and (on the Some arm) unique_distinct_kind() == first_distinct_kind() == last_distinct_kind() bind the exactly- one scalar identity to the widened primitives at the trait’s default body.

Peer to Self::unique_missing_kind

Closed-set-inversion peer of the exactly-one-hit scalar on the closed-set-complement axis — where unique_missing_kind names the SOLE ABSENT kind, unique_distinct_kind names the SOLE PRESENT kind. The two primitives close the (present, absent) x (endpoint, exactly-one) 2x3 scalar-Option grid on the slice level under the SAME two-step short-circuit shape via the load-bearing iterator peers.

Semantics

An empty slice returns None (0 distinct, not 1). A slice carrying a single ConditionKind (with any multiplicity) returns Some(k) — the SOLE arm where unique_distinct_kind returns Some on any N ≥ 2 closed set. A slice carrying K ≥ 2 distinct kinds returns None. A saturated slice returns None on N ≥ 2 closed sets.

Compounding future consumers

• A future singleton-coverage diagnostic that prints “the SOLE ConditionKind covered by this Boundary is X” reads boundary.postconditions.unique_distinct_kind() at ONE call site — the WITNESS + the exactly-one predicate composed at ONE short-circuit walk, rather than pairing the Boolean Self::has_unique_distinct_kind with Self::first_distinct_kind at TWO independent walks whose agreement is a coincidence.
• A unique-distinct-<kind> require-tag classifier arm reads this primitive with no allocation, byte-for-byte symmetrical with slice.unique_missing_kind().
• A fast-path branch that discriminates “exactly one kind covered” from “0 or ≥ 2 covered” reads slice.unique_distinct_kind().is_some() at ONE call site.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The exactly-one-hit witnessing projection on the closed-set- inversion axis lives at ONE substrate site as a typed two- step-short-circuit fold through the load-bearing Self::iter_distinct_kinds iterator — byte-for-byte peer of the tagged-union crate::tagged_union::TaggedUnion::unique_populated_kind under the SAME iterator shape.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the short-circuit walk — a slice previously at the singleton-coverage arm (returned Some(k) here) that also picks up the new variant now has TWO distinct kinds and returns None.

fn has_multiple_distinct_kinds(&self) -> bool

Boolean cardinality many-arm peer of Self::has_unique_distinct_kind on the closed-set-inversion axis — true iff AT LEAST TWO ConditionKind::ALL variants appear at least once in this slice (equivalently, Self::distinct_kind_count >= 2 and Self::distinct_kinds.len() >= 2).

Default body: a two-step-short-circuit closed-set walk over Self::iter_distinct_kinds — pulls up to two hits off the load-bearing distinct iterator; the primitive returns true iff BOTH the first and the second are Some, WITHOUT materializing Self::distinct_kinds’s Vec and WITHOUT walking every slot to build Self::distinct_kind_count’s scalar. Short-circuits at the second distinct kind — strictly cheaper than either widened primitive on every arm with ≥ 2 distinct kinds. Byte-for-byte peer of crate::tagged_union::TaggedUnion::has_multiple_populated_kinds under the (populated, missing) inversion axis one struct-layer up.

Peer to crate::tagged_union::TaggedUnion::has_multiple_populated_kinds

Slice-level peer of the tagged-union parent-level cardinality many-arm predicate one struct-layer up: where crate::tagged_union::TaggedUnion::has_multiple_populated_kinds answers “are AT LEAST TWO slots on the tagged-union parent occupied?”, has_multiple_distinct_kinds answers “do AT LEAST TWO kinds appear in AT LEAST ONE condition of the slice?”. Both compose against a two-step-short-circuit closed-set walk under a presence predicate (has(kind) / has_kind(kind)) at two adjacent typescape sites — the two primitives close the at- least-two arm on the closed-set-inversion axis at both struct layers under the SAME shape.

Sibling to the Boolean distinct-cardinality trichotomy

Third and final arm of the {0, 1, ≥2} cardinality trichotomy on the distinct axis at the slice level, closing the natural partition alongside the zero-arm (the empty-distinct endpoint, reached via !has_any_distinct_kind()) and Self::has_unique_distinct_kind (one-arm). Every slice satisfies EXACTLY ONE of the three Boolean projections — the three primitives partition 0..=ConditionKind::ALL.len() at 0, 1, and ≥ 2 respectively. The composition law has_multiple_distinct_kinds() == (distinct_kind_count() >= 2) binds the Boolean projection to the scalar primitive at the trait’s default body — swept substrate-wide by assert_slice_refinement_composition_laws as its distinct-cardinality-many-arm arm.

Semantics

An empty slice returns false (0 distinct, not ≥ 2). A slice carrying a single ConditionKind (with any multiplicity) returns false (1 distinct, not ≥ 2). A slice carrying K ≥ 2 distinct kinds returns true. A saturated slice returns true on any N ≥ 2 closed set (every kind present, ≥ 2 ≥ 2).

Compounding future consumers

• An operator-facing “≥ 2 dependencies covered” fast-path discriminator on the many-distinct arm reads boundary.postconditions.has_multiple_distinct_kinds() at ONE call site — one two-step short-circuit walk, no allocation, no scalar comparison against >= 2, byte-for- byte peer of the tagged-union has-multiple-populated-kinds classifier one struct-layer up under the SAME two-step short-circuit shape.
• A has-multiple-distinct-kinds require-tag classifier arm reaches this primitive with no allocation, byte-for-byte peer of the tagged-union has-multiple-populated-kinds classifier one struct-layer up.
• A future multi-coverage diagnostic that prints “≥ 2 distinct ConditionKinds covered by this Boundary” reads has_multiple_distinct_kinds() at ONE call site without allocating Self::distinct_kinds’s Vec.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The cardinality-many-arm projection on the distinct axis lives at ONE substrate site as a typed two-step-short-circuit fold through the load-bearing Self::iter_distinct_kinds iterator — byte-for-byte peer of distinct_kind_count() composed against >= 2, but with a second-distinct-slot short-circuit that the scalar counter primitive does not offer.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the short-circuit walk — a slice previously at the singleton-coverage arm (returned false here) that also picks up the new variant now has TWO distinct kinds and flips to true.

fn has_at_most_one_distinct_kind(&self) -> bool

Boolean cardinality “≤ 1” negation peer of Self::has_multiple_distinct_kinds on the closed-set-inversion axis — true iff AT MOST ONE ConditionKind::ALL variant appears at least once in this slice (equivalently, Self::distinct_kind_count <= 1 and Self::distinct_kinds.len() <= 1). Closes the {0, 1, ≥2, ≤1} Boolean-negation grid on the distinct axis at the slice level alongside its sibling has_multiple_distinct_kinds (≥ 2 many- arm) under the definitional negation !(≥ 2) == (≤ 1), and alongside !has_any_distinct_kind (=0 empty-endpoint) OR has_unique_distinct_kind (=1 mid-endpoint) as the trichotomy- union arm. Names the arrangement space where the slice is EMPTY-OR-SINGLETON (zero or exactly one distinct kind).

Default body: !self.has_multiple_distinct_kinds() — a definitional Boolean negation of the many-arm primitive. Short- circuits transitively through Self::has_multiple_distinct_kinds’s two-step short-circuit walk over Self::iter_distinct_kinds: returns true as soon as the many-arm walk stops with fewer than two distinct hits, WITHOUT materializing Self::distinct_kinds’s Vec and WITHOUT walking every slot to build Self::distinct_kind_count’s scalar. Byte-for-byte peer of crate::tagged_union::TaggedUnion::has_at_most_one_populated_kind under the (populated, missing) inversion axis one struct-layer up, both composed as the same definitional negation of their respective many-arm primitives.

Peer to crate::tagged_union::TaggedUnion::has_at_most_one_populated_kind

Slice-level peer of the tagged-union parent-level cardinality “≤ 1” predicate one struct-layer up: where crate::tagged_union::TaggedUnion::has_at_most_one_populated_kind answers “does the tagged-union parent have AT MOST ONE occupied slot?”, has_at_most_one_distinct_kind answers “do AT MOST ONE kind appear in AT LEAST ONE condition of the slice?”. Both compose as the definitional Boolean negation of their many-arm primitive (!has_multiple_populated_kinds() / !has_multiple_distinct_kinds()) at two adjacent typescape sites — the two primitives close the “≤ 1” arm on the closed- set-inversion axis at both struct layers under the SAME shape.

Peer to Self::has_at_most_one_missing_kind

Axis-parity mirror of the closed-set-complement “≤ 1” negation peer at the slice level — where has_at_most_one_missing_kind tests “at most one kind MISSING” (near-saturation-or-saturated), has_at_most_one_distinct_kind tests “at most one kind PRESENT” (empty-or-singleton). Both compose the same definitional negation shape (!has_multiple_*_kinds()) at the slice-level trait’s default body — the two primitives close the “≤ 1” arm on both the closed-set-complement and closed-set- inversion axes at the SAME struct layer under the SAME shape.

Sibling to the Boolean distinct-cardinality tetrachotomy

Fourth arm of the {0, ≥1, 1, ≥2, ≤1} Boolean-cardinality closure on the distinct axis at the slice level, closing the Boolean-negation grid alongside !has_any_distinct_kind (=0 zero-arm reached via Self::has_any_distinct_kind), Self::has_unique_distinct_kind (=1 mid-endpoint), Self::has_any_distinct_kind (≥1 halfspace), and Self::has_multiple_distinct_kinds (≥2 many-arm). The {≤1, ≥2} pair sit on the Boolean-negation axis: has_at_most_one_distinct_kind == !has_multiple_distinct_kinds on every arm. The {0, 1} union arm sits on the trichotomy-union axis: has_at_most_one_distinct_kind == !has_any_distinct_kind || has_unique_distinct_kind on every arm. Both composition laws bind the “≤ 1” Boolean projection to the sibling primitives at the trait’s default body — swept substrate-wide by assert_slice_refinement_composition_laws as its distinct- axis “≤ 1” arm.

Semantics

An empty slice returns true (0 distinct, ≤ 1) — the dual of the empty-slice arm on Self::has_at_most_one_missing_kind which returns false on N ≥ 2 closed sets (empty means every kind missing, N ≥ 2 missing, not ≤ 1). A slice carrying a single ConditionKind (with any multiplicity) returns true (1 distinct, ≤ 1) — the singleton arm on the distinct axis. A slice carrying K ≥ 2 distinct kinds returns false. A saturated slice returns false on any N ≥ 2 closed set (every kind present, N ≥ 2 distinct, not ≤ 1) — the union of the two “≤ 1” arms (=0 and =1) is exactly the arrangement space where the primitive returns true.

Compounding future consumers

• An operator-facing “at most one dependency currently covered” fast-path discriminator on the empty / singleton-coverage arms reads boundary.postconditions.has_at_most_one_distinct_kind() at ONE call site — one bit-flip on the many-arm’s two-step short-circuit walk, no allocation, no scalar comparison against <= 1, byte-for-byte peer of the tagged-union has-at-most-one-populated-kind classifier one struct-layer up under the SAME !has_multiple_populated_kinds definitional negation shape.
• A has-at-most-one-distinct-kind require-tag classifier arm reaches this primitive with no allocation, closing the {0, 1, ≥ 2, ≤ 1} cardinality-Boolean grid on the distinct axis at the slice level alongside its sibling has-multiple-distinct-kinds under the Boolean negation axis and the missing-axis peer has-at-most-one-missing-kind under the closed-set-inversion axis.
• A future under-coverage diagnostic that says “at most one ConditionKind covered by this Boundary” reads has_at_most_one_distinct_kind() at ONE call site without allocating Self::distinct_kinds’s Vec.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The cardinality “≤ 1” projection on the distinct axis lives at ONE substrate site as the definitional Boolean negation of Self::has_multiple_distinct_kinds; the three composition forms (!has_multiple_distinct_kinds(), distinct_kind_count() <= 1, and !has_any_distinct_kind() || has_unique_distinct_kind()) compose through the SAME two- step-short-circuit walk shape one negation up, byte-for-byte identical on every arm.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the delegated Self::has_multiple_distinct_kinds — a slice previously at the singleton arm (returned true here) that also picks up the new variant now has TWO distinct kinds and flips to false.

fn has_any_missing_kind(&self) -> bool

Boolean at-least-one halfspace peer of Self::is_kind_saturated on the closed-set-complement axis — true iff AT LEAST ONE ConditionKind::ALL variant appears zero times in this slice (equivalently, Self::missing_kinds is non-empty, Self::missing_kind_count > 0, Self::first_missing_kind is Some).

Default body: !self.is_kind_saturated() — a definitional negation of the saturation-endpoint primitive. Short-circuits transitively through Self::is_kind_saturated’s ConditionKind::ALL.iter().all(has_kind) composition: the underlying all walk returns false at the FIRST missing kind (yielding true here) WITHOUT materializing Self::missing_kinds’s Vec, WITHOUT walking every slot to build Self::missing_kind_count’s scalar, and WITHOUT allocating the closed-set-complement scan. Strictly cheaper than either widened primitive on every partially-populated arm.

Peer to crate::tagged_union::TaggedUnion::has_any_missing_kind

Slice-level peer of the tagged-union parent-level at-least-one halfspace predicate one struct-layer up: where crate::tagged_union::TaggedUnion::has_any_missing_kind answers “is ANY slot on the tagged-union parent empty?”, has_any_missing_kind answers “does ANY kind appear in NO condition of the slice?”. Both compose against their saturation-endpoint primitive under a definitional negation (!is_saturated / !is_kind_saturated) at two adjacent typescape sites — the two primitives close the at-least-one halfspace on the closed-set-complement axis at both struct layers under the SAME shape.

Sibling to Self::is_kind_saturated

Boolean at-least-one halfspace peer of the zero-arm saturation- endpoint primitive on the closed-set-complement axis — where is_kind_saturated returns true iff missing_kind_count == 0, has_any_missing_kind returns its Boolean-negation: true iff missing_kind_count >= 1. Together the two Booleans partition the missing-cardinality closed set: exactly one of is_kind_saturated() and has_any_missing_kind() is true for every slice. The definitional negation law has_any_missing_kind() == !is_kind_saturated() is pinned as a first-class typed invariant by the trait’s own default body and swept substrate-wide by assert_slice_refinement_composition_laws as its at-least- one halfspace arm.

Sibling to Self::missing_kinds / Self::missing_kind_count

Boolean at-least-one halfspace peer of the widened + scalar closed-set-complement primitives — where missing_kinds returns the FULL missing SET (a Vec<ConditionKind> of every absent kind) and missing_kind_count returns its cardinality (a usize in 0..=ConditionKind::ALL.len()), has_any_missing_kind collapses either the widened primitive to its non-emptiness Boolean or the scalar to its >= 1 halfspace Boolean. The composition laws has_any_missing_kind() == !missing_kinds().is_empty() and has_any_missing_kind() == (missing_kind_count() > 0) bind this Boolean projection to the widened + scalar primitives at the trait’s default body — strictly cheaper than either widened primitive on every partially-populated arm because the negation short-circuits at the first missing kind on the has-side walk rather than allocating the closed-set-complement scan or walking every slot to build the scalar cardinality.

Semantics

An empty slice returns true (every kind is missing — the fully-missing endpoint). A slice carrying a strict subset of ConditionKind::ALL returns true. A saturated slice returns false — the SOLE arm on which has_any_missing_kind returns false, byte-for-byte peer of the SOLE arm on which is_kind_saturated returns true.

Compounding future consumers

• A fleet-wide “gap present” fast-path that discriminates “some kind is missing” from “every kind is present” reads boundary.postconditions.has_any_missing_kind() at ONE call site rather than negating is_kind_saturated() at the callsite or restating missing_kind_count() > 0 (which walks every slot to count) or !missing_kinds().is_empty() (which allocates the Vec before the negated emptiness check).
• A has-any-missing-kind require-tag classifier arm reaches this primitive with no allocation, byte-for-byte peer of the tagged-union has-any-missing-kind classifier one struct- layer up under the SAME !is_saturated definitional negation shape.
• A coherence check that flags “any process boundary with a missing ConditionKind” reads boundary.postconditions.has_any_missing_kind() at ONE substrate primitive per test rather than restating the negation body at every callsite.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The at-least-one halfspace projection lives at ONE substrate site as a definitional negation of Self::is_kind_saturated. Every downstream consumer whose semantic reading is “at least one kind is absent” reads through this primitive rather than negating is_kind_saturated at every callsite or paying for the widened primitive’s Vec allocation.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the delegated is_kind_saturated — a slice that was previously saturated (returned false here) picks up the new missing variant and returns true at every downstream has-any-missing-kind callsite unless it also carries the new variant.

fn has_unique_missing_kind(&self) -> bool

Boolean cardinality-mid-endpoint peer of Self::has_any_missing_kind on the closed-set-complement axis — true iff EXACTLY ONE ConditionKind::ALL variant appears zero times in this slice (equivalently, Self::missing_kind_count == 1, Self::missing_kinds.len() == 1, and Self::first_missing_kind equals Self::last_missing_kind and is Some).

Default body: a two-step-short-circuit closed-set walk over ConditionKind::ALL under a negated Self::has_kind predicate. Pulls up to two hits off the filtered iterator; the primitive returns true iff the first hit is Some and the second is None, WITHOUT materializing Self::missing_kinds’s Vec and WITHOUT walking every slot to build Self::missing_kind_count’s scalar. Short-circuits at the SECOND missing kind — strictly cheaper than either widened primitive on every arm with ≥ 2 missing kinds.

Peer to crate::tagged_union::TaggedUnion::has_unique_missing_kind

Slice-level peer of the tagged-union parent-level cardinality-mid-endpoint predicate one struct-layer up: where crate::tagged_union::TaggedUnion::has_unique_missing_kind answers “is EXACTLY ONE slot on the tagged-union parent empty?”, has_unique_missing_kind answers “does EXACTLY ONE kind appear in NO condition of the slice?”. Both compose against a two-step-short-circuit closed-set walk under a negated presence predicate (!has(kind) / !has_kind(kind)) at two adjacent typescape sites — the two primitives close the exactly-one-arm on the closed-set-complement axis at both struct layers under the SAME shape.

Sibling to the Boolean missing-cardinality trichotomy

Second arm of the {0, 1, ≥2} cardinality trichotomy on the missing axis, closing the natural partition alongside Self::is_kind_saturated (zero-arm) and (once its slice- level peer lands) the many-arm predicate. Every slice satisfies EXACTLY ONE of the three Boolean projections — the three primitives partition 0..=ConditionKind::ALL.len() at 0, 1, and ≥ 2 respectively. The composition law has_unique_missing_kind() == (missing_kind_count() == 1) binds the Boolean projection to the scalar primitive at the trait’s default body — swept substrate-wide by assert_slice_refinement_composition_laws as its cardinality-mid-endpoint arm.

Semantics

An empty slice returns false on any N ≥ 2 closed set (every kind is missing — the fully-missing endpoint, N missing not 1). A slice carrying K distinct kinds for 1 ≤ K ≤ N-2 on N ≥ 3 closed sets returns false (N - K ≥ 2 kinds missing). A slice at the near-saturation arm (carrying every kind except exactly one) returns true — the SOLE arrangement where has_unique_missing_kind returns true. A saturated slice returns false (zero missing).

Compounding future consumers

• An operator-facing “one kind away from saturated” fast-path discriminator on the near-saturation arm reads boundary.postconditions.has_unique_missing_kind() at ONE call site — one two-step short-circuit walk, no allocation, no scalar equality against 1, byte-for-byte peer of the tagged-union has-unique-missing-kind classifier one struct- layer up under the SAME two-step short-circuit shape.
• A has-unique-missing-kind require-tag classifier arm reaches this primitive with no allocation, byte-for-byte peer of the tagged-union has-unique-missing-kind classifier one struct-layer up.
• A future gap-analysis diagnostic that prints “one remaining ConditionKind not covered by this Boundary” pairs has_unique_missing_kind() with Self::first_missing_kind to name the SOLE remaining hole without allocating Self::missing_kinds’s Vec.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The cardinality-mid-endpoint projection on the missing axis lives at ONE substrate site as a typed two-step-short- circuit walk over ConditionKind::ALL under negated Self::has_kind — byte-for-byte peer of missing_kind_count() composed against == 1, but with a second-missing-slot short-circuit that the scalar counter primitive does not offer.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the short-circuit walk — a slice previously at the near-saturation arm (returned true here) that omits the new variant now has TWO missing kinds and returns false; a slice previously at the saturated-except-one-of-two arm on an N == 2 closed set remains at the near-saturation arm on N ≥ 3 iff it picks up every OTHER variant.

fn unique_missing_kind(&self) -> Option<ConditionKind>

Witnessing Option<ConditionKind> peer of Self::has_unique_missing_kind on the closed-set-complement axis — Some(k) iff k is the SOLE ConditionKind::ALL variant ABSENT from this slice, else None.

Default body: a two-step-short-circuit fold through Self::iter_missing_kinds — pull the first hit; return Some(first) iff the second hit is None, else None. Byte-for-byte peer of crate::tagged_union::TaggedUnion::unique_missing_kind one struct-layer up under the SAME iter_missing_kinds two-step short-circuit shape, and the WITNESSING scalar peer of the Boolean Self::has_unique_missing_kind predicate at the SAME two-step short-circuit shape.

Sibling to Self::first_missing_kind / Self::last_missing_kind

FIFTH refinement on the closed-set-complement axis under exactly-one-hit semantics, Option<ConditionKind>-valued: together with Self::first_missing_kind and Self::last_missing_kind the three primitives project Self::missing_kinds onto its cardinality-conditioned scalar identity on the absent side. The composition laws unique_missing_kind().is_some() == (missing_kind_count() == 1) and (on the Some arm) unique_missing_kind() == first_missing_kind() == last_missing_kind() bind the exactly- one scalar identity to the widened primitives at the trait’s default body.

Peer to Self::unique_distinct_kind

Closed-set-complement peer of the exactly-one-hit scalar on the closed-set-inversion axis — where unique_distinct_kind names the SOLE PRESENT kind, unique_missing_kind names the SOLE ABSENT kind. The two primitives close the (present, absent) x (endpoint, exactly-one) 2x3 scalar-Option grid on the slice level under the SAME two-step short-circuit shape via the load-bearing iterator peers on the two opposite sides.

Semantics

An empty slice returns None on any N ≥ 2 closed set (every kind is missing — the fully-missing endpoint, N missing not 1). A slice at the near-saturation arm (carrying every kind except exactly one) returns Some(the-lone-empty) — the SOLE arm where unique_missing_kind returns Some on any N ≥ 3 closed set. A saturated slice returns None (zero missing).

Compounding future consumers

• An operator-facing “one dependency still unfulfilled: X” diagnostic on the near-saturation arm reads boundary.postconditions.unique_missing_kind() at ONE call site — the WITNESS + the exactly-one predicate composed at ONE short-circuit walk, rather than pairing the Boolean Self::has_unique_missing_kind with Self::first_missing_kind at TWO independent walks whose agreement is a coincidence.
• A unique-missing-<kind> require-tag classifier arm reads this primitive with no allocation, byte-for-byte symmetrical with slice.unique_distinct_kind().
• A fast-path branch that discriminates “exactly one kind still missing” from “0 or ≥ 2 still missing” reads slice.unique_missing_kind().is_some() at ONE call site.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The complement-exactly-one-hit witnessing projection lives at ONE substrate site as a typed two-step-short-circuit fold through the load-bearing Self::iter_missing_kinds iterator — byte-for-byte peer of the tagged-union crate::tagged_union::TaggedUnion::unique_missing_kind under the SAME iterator shape.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically on the missing side.

fn has_multiple_missing_kinds(&self) -> bool

Boolean cardinality “≥ 2” many-arm peer of Self::has_unique_missing_kind on the closed-set-complement axis — true iff AT LEAST TWO ConditionKind::ALL variants appear zero times in this slice (equivalently, Self::missing_kind_count >= 2 and Self::missing_kinds.len() >= 2).

Default body: a two-step-short-circuit closed-set walk over ConditionKind::ALL under a negated Self::has_kind predicate. Pulls up to two hits off the filtered iterator; the primitive returns true iff BOTH the first and the second are Some, WITHOUT materializing Self::missing_kinds’s Vec and WITHOUT walking every slot to build Self::missing_kind_count’s scalar. Short-circuits at the second missing kind — strictly cheaper than either widened primitive on every arm with ≥ 2 missing kinds. Byte-for-byte peer of crate::tagged_union::TaggedUnion::has_multiple_missing_kinds under the (populated, missing) complement axis one struct- layer up.

Peer to crate::tagged_union::TaggedUnion::has_multiple_missing_kinds

Slice-level peer of the tagged-union parent-level cardinality many-arm predicate one struct-layer up: where crate::tagged_union::TaggedUnion::has_multiple_missing_kinds answers “are AT LEAST TWO slots on the tagged-union parent empty?”, has_multiple_missing_kinds answers “do AT LEAST TWO kinds appear in NO condition of the slice?”. Both compose against a two-step-short-circuit closed-set walk under a negated presence predicate (!has(kind) / !has_kind(kind)) at two adjacent typescape sites — the two primitives close the at-least-two arm on the closed-set-complement axis at both struct layers under the SAME shape.

Sibling to the Boolean missing-cardinality trichotomy

Third and final arm of the {0, 1, ≥2} cardinality trichotomy on the missing axis at the slice level, closing the natural partition alongside Self::is_kind_saturated (zero-arm) and Self::has_unique_missing_kind (one-arm). Every slice satisfies EXACTLY ONE of the three Boolean projections — the three primitives partition 0..=ConditionKind::ALL.len() at 0, 1, and ≥ 2 respectively. The composition law has_multiple_missing_kinds() == (missing_kind_count() >= 2) binds the Boolean projection to the scalar primitive at the trait’s default body — swept substrate-wide by assert_slice_refinement_composition_laws as its cardinality-many-arm arm.

Semantics

An empty slice returns true on any N ≥ 2 closed set (every kind is missing — the fully-missing endpoint, N ≥ 2 missing). A slice carrying K distinct kinds for 1 ≤ K ≤ N-2 on N ≥ 3 closed sets returns true (N - K ≥ 2 kinds missing). A slice at the near-saturation arm (carrying every kind except exactly one) returns false — the SOLE-missing arrangement where has_multiple_missing_kinds returns false (exactly one missing, not ≥ 2). A saturated slice returns false (zero missing).

Compounding future consumers

• An operator-facing “≥ 2 dependencies still unfulfilled” fast- path discriminator on the many-missing arm reads boundary.postconditions.has_multiple_missing_kinds() at ONE call site — one two-step short-circuit walk, no allocation, no scalar comparison against >= 2, byte-for-byte peer of the tagged-union has-multiple-missing-kinds classifier one struct-layer up under the SAME two-step short-circuit shape.
• A has-multiple-missing-kinds require-tag classifier arm reaches this primitive with no allocation, byte-for-byte peer of the tagged-union has-multiple-missing-kinds classifier one struct-layer up.
• A future coverage-gap diagnostic that says “≥ 2 remaining ConditionKinds not covered by this Boundary” reads has_multiple_missing_kinds() at ONE call site without allocating Self::missing_kinds’s Vec.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The cardinality-many-arm projection on the missing axis lives at ONE substrate site as a typed two-step-short- circuit walk over ConditionKind::ALL under negated Self::has_kind — byte-for-byte peer of missing_kind_count() composed against >= 2, but with a second-missing-slot short-circuit that the scalar counter primitive does not offer.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the short-circuit walk — a slice previously at the near-saturation arm (returned false here) that omits the new variant now has TWO missing kinds and flips to true; a slice previously at the saturated arm on an N == 2 closed set that omits the new variant flips from false to true (1 ≥ 2 false → 1 missing on N == 3, but this workspace has N == 8, so the flip surfaces well before the endpoint).

fn has_at_most_one_missing_kind(&self) -> bool

Boolean cardinality “≤ 1” negation peer of Self::has_multiple_missing_kinds on the closed-set-complement axis — true iff AT MOST ONE ConditionKind::ALL variant appears zero times in this slice (equivalently, Self::missing_kind_count <= 1 and Self::missing_kinds.len() <= 1). Names the arm where the slice is SATURATED-OR-NEAR-SATURATED (zero or exactly one kind missing).

Default body: !self.has_multiple_missing_kinds() — a definitional Boolean negation of the many-arm primitive. Short- circuits transitively through Self::has_multiple_missing_kinds’s two-step short-circuit closed-set walk: returns true as soon as the many-arm walk stops with fewer than two missing hits, WITHOUT materializing Self::missing_kinds’s Vec and WITHOUT walking every slot to build Self::missing_kind_count’s scalar. Byte-for-byte peer of crate::tagged_union::TaggedUnion::has_at_most_one_missing_kind under the (populated, missing) complement axis one struct-layer up, both composed as the same definitional negation of their respective many-arm primitives.

Peer to crate::tagged_union::TaggedUnion::has_at_most_one_missing_kind

Slice-level peer of the tagged-union parent-level cardinality “≤ 1” predicate one struct-layer up: where crate::tagged_union::TaggedUnion::has_at_most_one_missing_kind answers “does the tagged-union parent have AT MOST ONE empty slot?”, has_at_most_one_missing_kind answers “do AT MOST ONE kind appear in NO condition of the slice?”. Both compose as the definitional Boolean negation of their many-arm primitive (!has_multiple_missing_kinds()) at two adjacent typescape sites — the two primitives close the “≤ 1” arm on the closed- set-complement axis at both struct layers under the SAME shape.

Sibling to the Boolean missing-cardinality pentachotomy

Fourth arm of the {0, 1, ≥1, ≤1, ≥2} Boolean-cardinality pentachotomy on the missing axis at the slice level, closing the Boolean-negation grid alongside Self::is_kind_saturated (=0 zero-arm), Self::has_unique_missing_kind (=1 mid-endpoint), Self::has_any_missing_kind (≥1 halfspace), and Self::has_multiple_missing_kinds (≥2 many-arm). The {≤1, ≥2} pair sit on the Boolean-negation axis: has_at_most_one_missing_kind == !has_multiple_missing_kinds on every arm. The {0, 1} union arm sits on the trichotomy-union axis: has_at_most_one_missing_kind == is_kind_saturated || has_unique_missing_kind on every arm. Both composition laws bind the “≤ 1” Boolean projection to the sibling primitives at the trait’s default body — swept substrate-wide by assert_slice_refinement_composition_laws as its “≤ 1” arm.

Semantics

An empty slice returns false on any N ≥ 2 closed set (every kind is missing — N ≥ 2 missing, not ≤ 1). A slice carrying K distinct kinds for 1 ≤ K ≤ N-2 on N ≥ 3 closed sets returns false (N - K ≥ 2 kinds missing). A slice at the near-saturation arm (carrying every kind except exactly one) returns true (exactly 1 missing, ≤ 1). A saturated slice returns true (0 missing, ≤ 1) — the union of the two “≤ 1” arms (=0 and =1) is exactly the arrangement space where the primitive returns true.

Compounding future consumers

• An operator-facing “at most one dependency still unfulfilled” fast-path discriminator on the near-saturated / saturated arms reads boundary.postconditions.has_at_most_one_missing_kind() at ONE call site — one bit-flip on the many-arm’s two-step short-circuit walk, no allocation, no scalar comparison against <= 1, byte-for-byte peer of the tagged-union has-at-most-one-missing-kind classifier one struct-layer up under the SAME !has_multiple_missing_kinds definitional negation shape.
• A has-at-most-one-missing-kind require-tag classifier arm reaches this primitive with no allocation, closing the {0, 1, ≥ 2, ≤ 1} cardinality-Boolean grid on the missing axis at the slice level alongside its sibling has-multiple-missing-kinds under the Boolean negation axis.
• A future coverage-gap diagnostic that says “at most one remaining ConditionKind not covered by this Boundary” reads has_at_most_one_missing_kind() at ONE call site without allocating Self::missing_kinds’s Vec.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The cardinality “≤ 1” projection on the missing axis lives at ONE substrate site as the definitional Boolean negation of Self::has_multiple_missing_kinds; the three composition forms (!has_multiple_missing_kinds(), missing_kind_count() <= 1, and is_kind_saturated() || has_unique_missing_kind()) compose through the SAME two-step-short-circuit walk shape one negation up, byte-for-byte identical on every arm.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the delegated Self::has_multiple_missing_kinds — a slice previously at the near-saturation arm (returned true here) that omits the new variant now has TWO missing kinds and flips to false.

fn lacks_kind(&self, kind: ConditionKind) -> bool

Boolean per-kind complement of Self::has_kind — true iff NO Condition in this slice carries the given ConditionKind (equivalently, the kind is a member of Self::missing_kinds).

Default body: !self.has_kind(kind) — a definitional negation of the presence-probe primitive. Short-circuits transitively through Self::has_kind’s composition down to Self::iter_kind: !self.find_kind(kind).is_some() returns as soon as any match is found (yielding false) without walking the rest of the slice, WITHOUT materializing Self::missing_kinds’s Vec per-kind for a per-kind question, and WITHOUT allocating the closed-set-complement scan.

Peer to crate::tagged_union::TaggedUnion::lacks

Slice-level peer of the tagged-union parent-level closed-set- complement predicate one struct-layer up: where crate::tagged_union::TaggedUnion::lacks answers “is THIS kind’s slot on the tagged-union parent empty?”, lacks_kind answers “does THIS kind appear in NO condition of the slice?”. Both compose against their per-kind presence primitive under a definitional negation (!has(kind) / !has_kind(kind)) at two adjacent typescape sites — the two primitives close the closed-set-complement invariant on the per-kind axis at both struct layers under the SAME shape.

Sibling to Self::has_kind

Boolean per-kind complement peer of the point-probe primitive on the closed-set-complement axis — where has_kind returns true iff the addressed kind appears at least once, lacks_kind returns its negation: true iff the addressed kind appears zero times. Together the two Booleans partition the (slice, kind) matrix at the slice-level presence-probe axis: exactly one of has_kind(k) and lacks_kind(k) is true for every k ∈ ConditionKind::ALL. The definitional complement law lacks_kind(k) == !has_kind(k) is pinned as a first-class typed invariant by the trait’s own default body and swept substrate- wide by assert_slice_refinement_composition_laws as its per-kind-complement arm.

Sibling to Self::missing_kinds / Self::missing_kind_count

Per-kind Boolean projection of the closed-set-complement widened + scalar primitives — where missing_kinds returns the FULL missing-set (a Vec<ConditionKind> of every absent kind) and missing_kind_count returns its cardinality (a usize in 0..=ConditionKind::ALL.len()), lacks_kind collapses the missing-set to its per-kind membership Boolean for ONE addressed kind. The composition law lacks_kind(k) == missing_kinds().contains(&k) binds this Boolean projection to the widened closed-set-complement primitive at the trait’s default body — strictly cheaper than the widened primitive on every per-kind question because the negation short-circuits at the first match on the has-side walk rather than allocating the closed-set-complement scan.

Semantics

An empty slice returns true for every ConditionKind (no kind appears, so every kind is lacked). A slice carrying kind k at any position returns false for lacks_kind(k) and true for lacks_kind(k') for every k' ≠ k (single-kind coverage). A saturated slice (every kind appears at least once) returns false on every arm — the SOLE arrangement where the primitive returns false for every kind.

Compounding future consumers

• A lacks-<kind> require-tag classifier arm reaches this primitive with no allocation, byte-for-byte peer of the tagged-union lacks-<kind> classifier one struct-layer up under the SAME !has(kind) definitional negation shape.
• A dependency-satisfaction coherence check that enforces “no process boundary lacks a ClosedLoopAuth postcondition” reads boundary.postconditions.lacks_kind(ConditionKind::ClosedLoopAuth) at ONE call site rather than negating boundary.postconditions.has_kind(ConditionKind::ClosedLoopAuth) at the callsite or materializing the closed-set complement with missing_kinds().contains(&k).
• A “still missing: ” diagnostic that reports the FIRST unmet postcondition kind reads slice.lacks_kind(k) inside a ConditionKind::ALL fold at ONE substrate primitive per test rather than restating the negation body at every callsite.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The per-kind closed-set-complement projection lives at ONE substrate site as a definitional negation of Self::has_kind. Every downstream consumer whose semantic reading is “the missing set contains THIS kind” reads through this primitive rather than negating has_kind at every callsite or paying for the closed-set-complement scan.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the delegated has_kind — every downstream lacks-<kind> classifier arm sees the wider kind set without further per-caller edit.

fn has_only_kind(&self, kind: ConditionKind) -> bool

Kind-scoped strict refinement of Self::has_kind — true iff the given kind appears in the slice AND no OTHER ConditionKind appears alongside it. The “exactly this one variant is present” predicate at the slice level.

Default body: a FUSED short-circuit closed-set walk over ConditionKind::ALL under Self::has_kind that returns false at the EARLIEST populated slot whose kind is NOT kind, and returns true iff the sweep completes with kind seen as the sole populated slot. Byte-for-byte cheaper than either widened composition self.distinct_kinds() == vec![kind] (which allocates the distinct-kind Vec before the equality test) or self.has_kind(kind) && self.distinct_kind_count() == 1 (which walks the closed-set twice) on every arm where the slice carries a populated kind that isn’t kind.

Peer to crate::tagged_union::TaggedUnion::has_only

Slice-level peer of the tagged-union parent-level kind-scoped strict-refinement predicate one struct-layer up: where crate::tagged_union::TaggedUnion::has_only answers “is THIS kind’s slot on the tagged-union parent the sole populated slot?”, has_only_kind answers “is THIS kind the sole distinct kind appearing in the slice?”. Both primitives compose the SAME fused short-circuit closed-set walk under a per-kind Self::has_kind / TaggedUnion::has predicate at two adjacent typescape sites — the two primitives close the kind-scoped strict-refinement invariant on the well-formed (1-of-N populated) arm at both struct layers under the SAME shape.

Sibling to Self::has_kind

Kind-scoped strict-refinement peer of the point-probe primitive on the closed-set-inversion axis — where has_kind(k) returns true iff k appears at least once (multiplicity ignored), has_only_kind(k) refines that to the strictly stricter predicate “k appears AND no other kind appears”. The implication chain has_only_kind(k) ⟹ has_kind(k) is a definitional consequence of the fused walk’s saw_kind = true arm; the reverse is FALSE on any partially-populated slice where a second kind lives alongside k. The composition law has_only_kind(k) == (distinct_kinds() == vec![k]) binds this primitive to the widened closed-set-inversion primitive at the trait’s default body — swept substrate-wide by assert_slice_refinement_composition_laws as its kind-scoped strict-refinement arm.

Truth table on the slice-level closed-set-inversion contract

For a slice with ConditionKind::ALL of cardinality N ≥ 2 and a fixed argument kind:

• Empty slice (0 conditions, distinct-kind set empty): false on any N ≥ 2 — no kind appears, so kind isn’t the sole populated kind.
• Single-populated slice with populated kind p (1 condition, distinct-kind set {p}): has_only_kind(kind) == (kind == p).
• Duplicate-populated slice with kind p at every position (multiplicity > 1, distinct-kind set {p}): still has_only_kind(kind) == (kind == p) — MULTIPLICITY IS IGNORED on the populated side (byte-for-byte with has_kind’s multiplicity behavior).
• Two-kinds slice with kinds {p, q} where p != q (distinct- kind set {p, q}): false for every kind — the strict refinement fails at the earliest walk step that hits the second kind.
• Saturated slice (every kind appears): false for every kind on any N ≥ 2 — N distinct kinds populate, so no single kind is “only”.

Kind-domain exhaustivity

A slice satisfies has_only_kind(k) for AT MOST one k, since two distinct kinds cannot both be the sole distinct populated kind. On the well-formed arm the count is exactly 1 (the addressed populated kind); on every other arm the count is 0. This kind-domain exhaustivity law binds the argument-scoped projection to the parent-scoped cardinality primitive distinct_kind_count() == 1 at the composition-law surface.

Compounding future consumers

• A has-only-<kind> require-tag classifier arm reaches this primitive with no allocation, byte-for-byte peer of the tagged-union has-only-<kind> classifier one struct-layer up under the SAME fused short-circuit walk shape.
• A coherence check verifying “every ephemeral spec whose postconditions carry ONLY ClosedLoopAuth (no JobAttested, no Cel, …) is a well-formed closed-loop probe” reads spec.postconditions.has_only_kind(ConditionKind::ClosedLoopAuth) at ONE call site — strictly cheaper than reaching for the widened composition on every well-formed-diagonal question.
• An operator-facing “unambiguously kind=” diagnostic on the slice-level probe reads slice.has_only_kind(k) after first_distinct_kind names the sole populated kind — one fused walk, no allocation, no Option<ConditionKind> construction.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The kind-scoped strict-refinement projection lives at ONE substrate site as a fused short-circuit walk over ConditionKind::ALL under Self::has_kind with early exit on the first populated slot whose kind is not kind — byte-for-byte cheaper than the widened composition distinct_kinds() == vec![kind], semantically identical on every arm.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the fused walk — every downstream has-only-<kind> classifier arm sees the wider kind set without further per-caller edit.

fn lacks_only_kind(&self, kind: ConditionKind) -> bool

Kind-scoped strict refinement of Self::lacks_kind — true iff the given kind does NOT appear in the slice AND every OTHER ConditionKind DOES appear at least once. The “exactly this one variant is the sole hole” predicate at the slice level.

Default body: a FUSED short-circuit closed-set walk over ConditionKind::ALL under Self::has_kind that skips every populated slot, returns false at the EARLIEST missing slot whose kind is NOT kind, and returns true iff the sweep completes with kind seen as the sole missing slot. Byte-for- byte cheaper than either widened composition self.missing_kinds() == vec![kind] (which allocates the missing-kind Vec before the equality test) or self.lacks_kind(kind) && self.missing_kind_count() == 1 (which walks the closed-set-complement scan twice) on every arm where the slice carries a missing kind that isn’t kind.

Peer to crate::tagged_union::TaggedUnion::lacks_only

Slice-level peer of the tagged-union parent-level kind-scoped strict-refinement predicate on the missing axis one struct-layer up: where crate::tagged_union::TaggedUnion::lacks_only answers “is THIS kind’s slot on the tagged-union parent the sole empty slot?”, lacks_only_kind answers “is THIS kind the sole missing kind from the slice’s distinct set?”. Both primitives compose the SAME fused short-circuit closed-set walk under a per-kind Self::has_kind / TaggedUnion::has predicate at two adjacent typescape sites — the two primitives close the kind-scoped strict-refinement invariant on the near-saturation-diagonal (N-1-of-N populated with the sole hole at kind) arm at both struct layers under the SAME shape.

Sibling to Self::has_only_kind

Closed-set-complement mirror of the well-formed-diagonal strict-refinement primitive on the populated axis — where has_only_kind(k) returns true iff k is the sole distinct populated kind, lacks_only_kind(k) returns true iff k is the sole missing kind. Together the two peers CLOSE the (populated, missing) × (subset, equal) 2x2 kind-scoped strict-refinement grid at the slice level alongside has_kind (populated subset) and lacks_kind (missing subset).

Truth table on the slice-level closed-set-complement contract

For a slice with ConditionKind::ALL of cardinality N ≥ 2 and a fixed argument kind:

• Empty slice (0 conditions, distinct-kind set empty, missing-kind set == ALL): false on any N ≥ 2 — every kind is missing, so kind is NOT the sole missing kind.
• Single-populated slice with populated kind p (1 condition, missing-kind set == ALL \ {p}): false on any N ≥ 3 (N - 1 ≥ 2 missing kinds, no sole missing kind); on N == 2 the missing set is {q} where q ≠ p, so lacks_only_kind(kind) == (kind == q).
• Near-saturation slice with populated kinds ALL \ {q} (each kind except q populated, missing set {q}): the SOLE true arm — lacks_only_kind(kind) == (kind == q).
• Saturated slice (every kind appears): false on every kind — no kind is missing, so no kind is the sole missing kind.
• Multiplicity is ignored on the populated side: a slice carrying k at every position still has an empty missing set, or a missing set {k'} where k' ≠ k, byte-for-byte with the single-populated arrangement.

Kind-domain exhaustivity

A slice satisfies lacks_only_kind(k) for AT MOST one k, since two distinct kinds cannot both be the sole missing kind. On the near-saturation arm the count is exactly 1 (the sole missing kind); on every other arm the count is 0. This kind-domain exhaustivity law binds the argument-scoped projection to the parent-scoped cardinality primitive missing_kind_count() == 1 at the composition-law surface.

Compounding future consumers

• A lacks-only-<kind> require-tag classifier arm reaches this primitive with no allocation, byte-for-byte peer of the tagged-union lacks-only-<kind> classifier one struct-layer up under the SAME fused short-circuit walk shape.
• A “one dependency short: ” diagnostic on the aggregate boundary check reads slice.lacks_only_kind(k) at ONE call site — one fused short-circuit walk, no allocation, strictly cheaper than slice.first_missing_kind() == Some(k) && slice.missing_kind_count() == 1 which walks the closed-set-complement scan twice.
• A coherence check that verifies “the near-saturation slice from an all_but_one_kind_of(k) factory is unambiguously missing kind k” reads slice.lacks_only_kind(k) at ONE site — the strongest structural pin on the missing-side well-formed diagonal.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The kind-scoped strict-refinement projection on the missing axis lives at ONE substrate site as a fused short-circuit walk over ConditionKind::ALL under Self::has_kind with early exit on the first missing slot whose kind is not kind — byte-for-byte peer of Self::has_only_kind’s fused walk under complement, semantically identical to first_missing_kind() == Some(kind) && missing_kind_count() == 1 on every arm.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the delegated has_kind walk — every downstream lacks-only-<kind> classifier arm sees the wider kind set without further per-caller edit.

fn has_multiple_of_kind(&self, kind: ConditionKind) -> bool

Boolean cardinality “≥ 2” many-arm peer of Self::has_kind (≥ 1) and Self::lacks_kind (= 0) on the per-kind count axis — true iff AT LEAST TWO Condition values with the given kind appear in this slice (equivalently, Self::count_kind(kind) >= 2 and Self::iter_kind(kind).count() >= 2).

Default body: a two-step-short-circuit walk over Self::iter_kind(kind) — pulls up to two hits off the load-bearing per-kind iterator; the primitive returns true iff BOTH the first and the second are Some, WITHOUT walking every slot to build Self::count_kind’s scalar. Short-circuits at the second matching condition — strictly cheaper than Self::count_kind(kind) >= 2 on every arm with ≥ 2 matches. Byte-for-byte peer of Self::has_multiple_distinct_kinds under the (distinct- kinds axis, per-kind matches axis) parity: both compose the SAME two-step short-circuit shape one iterator over.

Sibling to Self::lacks_kind / Self::has_kind / Self::count_kind

Many-arm on the per-kind count axis alongside Self::lacks_kind (= 0 zero-endpoint) and Self::has_kind (≥ 1 halfspace) — the three Booleans project Self::count_kind(kind)’s scalar onto its {= 0, ≥ 1, ≥ 2} arms. The composition law has_multiple_of_kind(k) == (count_kind(k) >= 2) binds the per-kind many-arm Boolean projection to the scalar counter primitive at the trait’s default body — swept substrate-wide by assert_slice_refinement_composition_laws as its per- kind many-arm arm.

Semantics

An empty slice returns false on every kind (0 matches, not ≥ 2). A slice carrying kind exactly once (with any other kinds in any multiplicity) returns false on THAT kind (1 match). A slice carrying kind two or more times returns true on THAT kind. Multiplicity of OTHER kinds is irrelevant — the primitive projects the slice onto the per- kind count axis for the queried kind alone.

Compounding future consumers

• A boundary-well-formedness coherence check that rejects a Process whose preconditions carry duplicate ConditionKind::ProcessPhase entries reads boundary.preconditions.has_multiple_of_kind(ConditionKind::ProcessPhase) at ONE call site — one two-step short-circuit walk, no allocation, no scalar comparison against >= 2.
• A has-multiple-of-<kind> require-tag classifier arm reads this primitive with no allocation, byte-for-byte peer of the whole-slice has-multiple-distinct-kinds classifier one axis over under the SAME two-step short-circuit shape.
• A fleet-wide “duplicate condition detected” audit dump reads ConditionKind::ALL.into_iter().filter(|k| slice.has_multiple_of_kind(*k)) at ONE call site.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The per-kind cardinality-many-arm projection on the count axis lives at ONE substrate site as a typed two-step-short- circuit fold through the load-bearing Self::iter_kind iterator — byte-for-byte peer of count_kind(kind) composed against >= 2, but with a second-match short-circuit that the scalar counter primitive does not offer.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the per-kind iterator — a slice previously containing no conditions of the new kind returns false on it here, and picks up true the moment an operator authors a second matching condition.

fn has_unique_of_kind(&self, kind: ConditionKind) -> bool

Boolean cardinality “= 1” middle-arm peer of Self::lacks_kind (= 0) and Self::has_multiple_of_kind (≥ 2) on the per-kind count axis — true iff EXACTLY ONE Condition with the given kind appears in this slice (equivalently, Self::count_kind(kind) == 1 and Self::iter_kind(kind).count() == 1). Closes the {= 0, = 1, ≥ 2} per-kind cardinality Boolean trichotomy at the slice level; every state maps to EXACTLY ONE of the three arms.

Default body: a two-step-short-circuit walk over Self::iter_kind(kind) — pulls up to two hits off the load- bearing per-kind iterator; the primitive returns true iff the first is Some AND the second is None, WITHOUT walking every slot to build Self::count_kind’s scalar. Short- circuits at the second matching condition — strictly cheaper than Self::count_kind(kind) == 1 on every arm with ≥ 2 matches (the primitive returns false on the second hit without pulling further). Byte-for-byte peer of Self::has_multiple_of_kind under the (= 1, ≥ 2) count-axis duality: both compose the SAME two-step short-circuit walk shape, differing only in the second-hit predicate (Option::is_none here vs Option::is_some on the many- arm peer).

Sibling to Self::lacks_kind / Self::has_kind /

Self::has_multiple_of_kind / Self::count_kind

Middle arm on the per-kind count trichotomy alongside Self::lacks_kind (= 0 zero-endpoint) and Self::has_multiple_of_kind (≥ 2 many-arm) — the three Booleans PARTITION the per-kind cardinality scalar’s non- negative-integer arms: EXACTLY ONE of the three returns true on any given (slice, kind) pair. Peer of the tagged-union parent-level crate::tagged_union::TaggedUnion::has_unique_populated_kind on the whole-parent count axis one struct layer up (single populated slot vs single condition of a given kind). The composition laws has_unique_of_kind(k) == (count_kind(k) == 1), has_unique_of_kind(k) == (iter_kind(k).count() == 1), and has_unique_of_kind(k) == { iter_kind(k) two-step short-circuit } bind the per-kind mid-endpoint Boolean projection to the scalar counter primitive at the trait’s default body — swept substrate-wide by assert_slice_refinement_composition_laws as its per-kind mid-endpoint arm alongside the existing per- kind many-arm pin.

Semantics

An empty slice returns false on every kind (0 matches, not = 1). A slice carrying kind exactly once (with any other kinds in any multiplicity) returns true on THAT kind. A slice carrying kind two or more times returns false on THAT kind. Multiplicity of OTHER kinds is irrelevant — the primitive projects the slice onto the per-kind count axis for the queried kind alone. Together with lacks_kind and has_multiple_of_kind, the three arms cover every non- negative multiplicity: lacks_kind(k) ↔ 0 matches, has_unique_of_kind(k) ↔ 1 match, has_multiple_of_kind(k) ↔ ≥ 2 matches.

Compounding future consumers

• A boundary-well-formedness coherence check that enforces “every Process’s preconditions carry EXACTLY ONE ConditionKind::ProcessPhase entry” reads boundary.preconditions.has_unique_of_kind(ConditionKind::ProcessPhase) at ONE call site — one two-step short-circuit walk, no allocation, no scalar comparison against == 1.
• A has-unique-of-<kind> require-tag classifier arm reads this primitive with no allocation, byte-for-byte peer of has-multiple-of-<kind> under the SAME two-step short- circuit shape.
• A fleet-wide “exactly-one-of-kind detected” audit dump reads ConditionKind::ALL.into_iter().filter(|k| slice.has_unique_of_kind(*k)) at ONE call site.
• A future authoring-time linter that surfaces “operator intended a singleton condition but ended up with 0 or ≥ 2 entries” reaches the three-arm partition through !slice.has_unique_of_kind(k) for the negative arm and drills down to the specific missing/duplicate case through slice.lacks_kind(k) or slice.has_multiple_of_kind(k) without restating the walk.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The per-kind cardinality-mid-endpoint projection on the count axis lives at ONE substrate site as a typed two-step- short-circuit fold through the load-bearing Self::iter_kind iterator — byte-for-byte peer of count_kind(kind) composed against == 1, but with a second-match short-circuit that the scalar counter primitive does not offer.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the per-kind iterator — a slice previously containing no conditions of the new kind returns false on it here, and picks up true the moment an operator authors exactly ONE matching condition (and returns to false the moment a second one appears).

fn has_at_most_one_of_kind(&self, kind: ConditionKind) -> bool

Boolean cardinality “≤ 1” negation peer of Self::has_multiple_of_kind on the per-kind count axis — true iff AT MOST ONE Condition with the given kind appears in this slice (equivalently, Self::count_kind (kind) <= 1 and Self::iter_kind(kind).count() <= 1). Closes the {= 0, = 1, ≥ 1, ≥ 2, ≤ 1} Boolean-cardinality grid on the per-kind axis at the slice level alongside its sibling Self::has_multiple_of_kind (≥ 2 many-arm) under the definitional negation !(≥ 2) == (≤ 1), and alongside !has_kind (= 0 zero-endpoint) OR Self::has_unique_of_kind (= 1 mid-endpoint) as the trichotomy-union arm. Names the per-kind arrangement space where the slice is EMPTY-OR-SINGLETON for that kind (zero or exactly one match).

Default body: !self.has_multiple_of_kind(kind) — a definitional Boolean negation of the many-arm primitive. Short-circuits transitively through Self::has_multiple_of_kind’s two-step short-circuit walk over Self::iter_kind: returns true as soon as the many- arm walk stops with fewer than two matches, WITHOUT walking every slot to build Self::count_kind’s scalar. Strictly cheaper than Self::count_kind(kind) <= 1 on every arm with ≥ 2 matches (short-circuits at the second hit rather than counting further). Byte-for-byte peer of Self::has_at_most_one_distinct_kind and Self::has_at_most_one_missing_kind under the (distinct, missing, per-kind) parity: all three compose the SAME definitional negation shape (!has_multiple_*) at the slice- level trait’s default body, differing only in the many-arm primitive they negate.

Peer to Self::has_at_most_one_distinct_kind / Self::has_at_most_one_missing_kind

Third axis of the slice-level “≤ 1” negation triad. The distinct-axis peer negates the “≥ 2 distinct kinds present” many-arm; the missing-axis peer negates the “≥ 2 kinds missing” many-arm; this per-kind peer negates the “≥ 2 matches of a specific kind” many-arm. Together the three close the “≤ 1” arm on every cardinality axis (distinct-kind, missing-kind, per-kind count) at the SAME slice-level trait under the SAME definitional negation shape.

Sibling to the per-kind Boolean cardinality tetrachotomy

Fourth arm of the {= 0, ≥ 1, = 1, ≥ 2, ≤ 1} Boolean- cardinality closure on the per-kind axis at the slice level, closing the Boolean-negation grid alongside Self::lacks_kind (= 0 zero-endpoint), Self::has_unique_of_kind (= 1 mid-endpoint), Self::has_kind (≥ 1 halfspace), and Self::has_multiple_of_kind (≥ 2 many-arm). The {≤ 1, ≥ 2} pair sit on the Boolean-negation axis: has_at_most_one_of_kind(k) == !has_multiple_of_kind(k) on every arm. The {0, 1} union arm sits on the trichotomy-union axis: has_at_most_one_of_kind(k) == lacks_kind(k) || has_unique_of_kind(k) on every arm. Both composition laws bind the per-kind “≤ 1” Boolean projection to the sibling primitives at the trait’s default body — swept substrate-wide by assert_slice_refinement_composition_laws as its per- kind “≤ 1” arm alongside the existing per-kind zero-endpoint, mid-endpoint, halfspace, and many-arm pins.

Semantics

An empty slice returns true on every kind (0 matches, ≤ 1). A slice carrying kind exactly once (with any other kinds in any multiplicity) returns true on THAT kind. A slice carrying kind two or more times returns false on THAT kind. Multiplicity of OTHER kinds is irrelevant — the primitive projects the slice onto the per-kind count axis for the queried kind alone. Together with lacks_kind and has_unique_of_kind, the “≤ 1” arm equals their union: has_at_most_one_of_kind(k) ↔ lacks_kind(k) ∨ has_unique_of_kind(k).

Compounding future consumers

• A boundary-well-formedness coherence check that enforces “every Process’s preconditions carry AT MOST ONE ConditionKind::ProcessPhase entry” (allowing zero, but rejecting duplicates) reads boundary.preconditions.has_at_most_one_of_kind(ConditionKind::ProcessPhase) at ONE call site — one bit-flip on the many-arm’s two-step short-circuit walk, no allocation, no scalar comparison against <= 1. Byte-for-byte peer of the same coherence check phrased with !slice.has_multiple_of_kind(k) at the callsite, but reads the intent as “at most one” directly.
• A has-at-most-one-of-<kind> require-tag classifier arm reaches this primitive with no allocation, closing the {= 0, = 1, ≥ 1, ≥ 2, ≤ 1} cardinality-Boolean grid on the per-kind axis at the slice level alongside its sibling has-multiple-of-<kind> under the Boolean negation axis.
• A fleet-wide “no duplicate condition of kind detected” audit dump reads ConditionKind::ALL.into_iter().filter(|k| slice.has_at_most_one_of_kind(*k)) at ONE call site without materializing the negation at every callsite.
• A future authoring-time linter that surfaces “operator’s condition slice has no duplicates for any kind” reads ConditionKind::ALL.into_iter().all(|k| slice.has_at_most_one_of_kind(k)) — the whole-slice “no kind is duplicated” projection composes through the SAME substrate primitive without restating the negation.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The per-kind cardinality “≤ 1” projection lives at ONE substrate site as the definitional Boolean negation of Self::has_multiple_of_kind; the three composition forms (!has_multiple_of_kind(k), count_kind(k) <= 1, and lacks_kind(k) || has_unique_of_kind(k)) compose through the SAME two-step-short-circuit walk shape one negation up, byte-for-byte identical on every arm.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant added to ALL reaches this primitive mechanically through the delegated Self::has_multiple_of_kind — a slice previously at the empty or singleton arm (returned true here) that picks up a second condition of the new variant now has TWO matches and flips to false.

fn unique_of_kind(&self, kind: ConditionKind) -> Option<&Condition>

Returns the unique Condition of the given ConditionKind in this slice, or None if zero or more than one such Condition exists — the Option<&Condition> witnessing refinement of the Boolean Self::has_unique_of_kind on the per-kind count axis at the slice level. Default body: a two- step short-circuit walk over Self::iter_kind — pulls at most two matches, returns the first iff no second exists.

Sibling to Self::has_unique_of_kind

One refinement wider: has_unique_of_kind collapses the return to a bool; unique_of_kind returns the matching &Condition so callers can read Condition::params without a two-pass has+find dance. The composition laws has_unique_of_kind(k) == unique_of_kind(k).is_some() and unique_of_kind(k).map(|c| c.kind) == Some(k) (when has_unique_of_kind(k), else None) bind the Boolean projection to the widened witness at the trait’s default body.

Peer to Self::unique_distinct_kind / Self::unique_missing_kind

Third Option-witnessing peer on the slice-level Boolean mid-endpoint algebra: unique_distinct_kind witnesses the singleton-populated-distinct arm (Option<ConditionKind>), unique_missing_kind witnesses the singleton-missing arm (Option<ConditionKind>), and this per-kind peer witnesses the singleton-per-kind arm (Option<&Condition>). All three collapse has_unique_* Booleans to a single-walk Option witness of the singleton arm; a regression that drifted any witness from its Boolean sibling surfaces at the substrate’s composition-law testkit.

Semantics

An empty slice returns None on every kind. A slice carrying kind exactly once returns Some(&c) for that c. A slice carrying kind two or more times returns None (multiple witnesses collapse to no witness — the Option<&Condition> refinement expresses “there is exactly one match, and here it is” as a single type-carried invariant). Multiplicity of other kinds is irrelevant.

Compounding

A coherence check that verifies “if exactly one ConditionKind::PromQL precondition, its params must contain expr” reads slice.unique_of_kind(ConditionKind::PromQL).map(check_params) at ONE call site — one walk, no allocation, no two-pass has_unique_of_kind + find_kind dance that would walk the slice twice. A future operator-facing diagnostic that surfaces “the unique JobAttested condition’s params” reads spec.postconditions.unique_of_kind(JobAttested) and unwraps the params directly — a two-pass phrase leaves the singleton invariant implicit; this peer carries it in the return type.

Theory grounding

• THEORY.md §II.1 invariant 5 — composition preserves proofs. The Option<&Condition> witnessing refinement lives at ONE substrate site as a two-step short-circuit walk over Self::iter_kind; the composition law has_unique_of_kind(k) == unique_of_kind(k).is_some() binds the Boolean projection to the widened witness at the trait’s default body.
• THEORY.md §VI.1 — generation over composition. A new ConditionKind variant reaches this primitive mechanically through the delegated Self::iter_kind with no per-caller edit.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl ConditionSliceExt for [Condition]

fn iter_kind(&self, kind: ConditionKind) -> KindMatches<'_>

Implementors