From d0067fa76c5ceeca93e7bfeb4443a35a575769f7 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Fri, 7 Aug 2026 10:32:02 +0200 Subject: [PATCH] ogar-elk: the EL subsumption closure as the third factfinder MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `ogar-obo` and `ogar-ro` say what is ASSERTED. Nothing said what FOLLOWS. This closes that gap with the smallest calculus that does the job. Three rules over ABI-shaped (classid, identity) addresses: R1 reflexivity A ⊑ A R2 transitivity A ⊑ B , B ⊑ C ⟹ A ⊑ C R3 merge-soundness closing C ∪ S introduces no A ≡ B absent from C Two questions, no others: does `A ⊑ B` follow, and is adding a set of axioms to an existing closure sound. UNGRADED BY CONSTRUCTION. An EL entailment is a fact — it follows necessarily or it does not — so nothing here is scored, ranked or weighted. The thinking that consumes these facts lives one layer out and this crate is unfazed by it. ADDRESSES, NEVER A FILE. It never parses an ontology, resolves a CURIE, or reads a label. Reasoning over the addressed form is the whole point of having addressed it; a reasoner reaching back for the source document would re-introduce the coupling the bake exists to remove. R3 IS WHY THIS IS A CRATE and not a transitive-closure helper. Two independently authored sources can each be internally consistent and still disagree about a relation's DIRECTION. Merging them then derives A ⊑ B and B ⊑ A for classes neither source calls equivalent — and that cycle is the disagreement made mechanical. It is found at ANY distance, including cycles that close through a chain no pairwise comparison would think to check. `merge` does not mutate: it returns a verdict splitting axioms into corroborating / enriching / conflicting, so a caller decides after seeing it. Silence is reported as enrichment, never as disagreement — the distinction that separates "the other source is denser" from "the other source is wrong". THE BOUNDARY IS DELIBERATE AND NAMED. No existential restrictions, no role composition, no bottom propagation, no conjunction/disjunction/complement. Each becomes necessary the moment a typed cross-angle predicate enters the closure, and at that point the correct move is to wrap a full reasoner, not to grow this file. The concrete hazard it guards: without role composition, walking subsumption and part-of together derives FALSE ancestors — `A part_of B` with `B ⊑ C` does NOT give `A ⊑ C`. `Closure::from_asserted` therefore takes a `Subsumption` type rather than raw pairs, so a mixed edge set cannot be fed in by accident. The depth guard is reported (`depth_cap`) rather than silent, so a caller can tell "not entailed" from "the walk stopped" — different answers that must not be conflated. Zero-dependency, forbid(unsafe_code), clippy -D warnings clean. 8 tests, each carrying the input that would falsify it: transitivity paired with a must-NOT-entail case, the depth cap proven to bind AND to release, cycles proven detected AND absent on a non-trivial acyclic graph, the merge verdict proven to discriminate all three outcomes, and a pre-existing cycle proven not to be blamed on an innocent merge. DISCOVERY-MAP: D-ELK-FACTFINDER appended. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01KCGhDYoQBXs3poaR7sFuqp --- Cargo.toml | 1 + crates/ogar-elk/Cargo.toml | 16 ++ crates/ogar-elk/src/lib.rs | 486 +++++++++++++++++++++++++++++++++++++ docs/DISCOVERY-MAP.md | 30 +++ 4 files changed, 533 insertions(+) create mode 100644 crates/ogar-elk/Cargo.toml create mode 100644 crates/ogar-elk/src/lib.rs diff --git a/Cargo.toml b/Cargo.toml index dfcca5c..c3771a1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -33,6 +33,7 @@ members = [ "crates/ogar-blockly", "crates/ogar-loco", "crates/ogar-ro", + "crates/ogar-elk", "crates/ogar-osm", ] diff --git a/crates/ogar-elk/Cargo.toml b/crates/ogar-elk/Cargo.toml new file mode 100644 index 0000000..d2a3eaa --- /dev/null +++ b/crates/ogar-elk/Cargo.toml @@ -0,0 +1,16 @@ +[package] +name = "ogar-elk" +version.workspace = true +edition.workspace = true +license.workspace = true +repository.workspace = true +authors.workspace = true +rust-version.workspace = true +description = "The EL subsumption closure as a FACTFINDER over ABI-shaped addressed edges. Answers two questions and no others: does `A ⊑ B` follow from what is asserted, and is adding a set of axioms to an existing closure sound (does it introduce an equivalence cycle). Entailments are facts — they follow necessarily — so nothing here is graded, ranked, or scored. Zero-dependency; consumes `(classid, identity)` addresses, never a legacy ontology file." + +[features] +default = [] +serde = ["dep:serde"] + +[dependencies] +serde = { workspace = true, optional = true } diff --git a/crates/ogar-elk/src/lib.rs b/crates/ogar-elk/src/lib.rs new file mode 100644 index 0000000..c41194b --- /dev/null +++ b/crates/ogar-elk/src/lib.rs @@ -0,0 +1,486 @@ +//! `ogar-elk` — the EL subsumption closure as a **factfinder**. +//! +//! # What this is, and the two questions it answers +//! +//! Third member of the factfinder family beside [`ogar-obo`] (harvest) and +//! [`ogar-ro`] (the predicate palette). Those two say what is *asserted*; this +//! one says what *follows*. It answers exactly two questions: +//! +//! 1. **Does `A ⊑ B` follow** from the asserted edges? ([`Closure::entails`]) +//! 2. **Is adding a set of axioms sound** — does the merged closure introduce +//! an equivalence cycle that was not already there? ([`Closure::merge`]) +//! +//! Nothing here is graded, ranked, scored or weighted. An EL entailment is a +//! **fact**: it follows necessarily from the asserted set, or it does not. The +//! thinking that consumes these facts lives elsewhere; this crate is unfazed by +//! it. +//! +//! [`ogar-obo`]: https://docs.rs/ogar-obo +//! [`ogar-ro`]: https://docs.rs/ogar-ro +//! +//! # Addresses, never a file +//! +//! Input is `(classid, identity)` — the ABI-shaped address a baked row already +//! carries. This crate never parses an ontology document, never resolves a +//! CURIE, and never looks at a label. That is deliberate: reasoning over the +//! addressed form is the whole point of having addressed it, and a reasoner +//! that reached back for the source file would re-introduce the coupling the +//! bake exists to remove. +//! +//! # The fragment, stated precisely +//! +//! Three completion rules, which is the entire calculus for a pure subsumption +//! spine: +//! +//! ```text +//! R1 reflexivity A ⊑ A +//! R2 transitivity A ⊑ B , B ⊑ C ⟹ A ⊑ C +//! R3 merge-soundness closing C ∪ S introduces no A ≡ B (A ≠ B) absent from C +//! ``` +//! +//! R3 is the validation rule and the reason this crate exists rather than a +//! transitive-closure helper. Two independently authored sources can each be +//! internally consistent and still disagree about the DIRECTION of a relation; +//! merging them then derives `A ⊑ B` and `B ⊑ A`, i.e. `A ≡ B`, for classes +//! neither source calls equivalent. That cycle is the disagreement, made +//! mechanical — and it is found at **any distance**, including cycles that close +//! through a chain no pairwise comparison would think to check. +//! +//! # What is deliberately NOT here +//! +//! - **Existential restrictions** (`∃r.C`) +//! - **Role composition** (`part_of ∘ part_of ⊑ part_of`) +//! - **Bottom propagation** (unsatisfiability) +//! - **Conjunction, disjunction, complement, self-restriction** +//! +//! Each is a real part of EL++ and each is absent on purpose. They become +//! necessary the moment typed cross-angle edges (an `ogar-ro` predicate other +//! than subsumption) enter the closure — and at that point the correct move is +//! to wrap a full reasoner, not to grow this file. The boundary is named here so +//! a future session sees it as a decision rather than an oversight. +//! +//! **The concrete hazard that boundary guards:** without role composition, +//! walking subsumption and part-of edges together derives FALSE ancestors. +//! `A part_of B` and `B ⊑ C` does not give `A ⊑ C`. This crate cannot make that +//! mistake because it only ever ingests subsumptions — but a caller that feeds +//! it a mixed edge set can, so [`Closure::from_asserted`] takes subsumptions by +//! type rather than raw pairs. + +#![forbid(unsafe_code)] + +use std::collections::{HashMap, HashSet, VecDeque}; + +/// A class address: `(classid, identity)`, exactly as a baked row carries it. +/// +/// Ordered and hashable so a closure can index by it without a side table. It +/// carries no namespace, no CURIE and no label — resolving those is the +/// caller's business and none of this crate's. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +pub struct ClassAddr { + /// The row's classid. + pub classid: u32, + /// The row's identity within that class. + pub identity: u32, +} + +impl ClassAddr { + /// Construct an address. + #[must_use] + pub const fn new(classid: u32, identity: u32) -> Self { + Self { classid, identity } + } +} + +/// An asserted subsumption `sub ⊑ sup`. +/// +/// A distinct type rather than a `(ClassAddr, ClassAddr)` tuple, so a caller +/// cannot hand this crate a `part_of` edge by accident — see the crate doc's +/// false-ancestor hazard. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +pub struct Subsumption { + /// The subclass. + pub sub: ClassAddr, + /// The superclass. + pub sup: ClassAddr, +} + +impl Subsumption { + /// Construct a subsumption. + #[must_use] + pub const fn new(sub: ClassAddr, sup: ClassAddr) -> Self { + Self { sub, sup } + } +} + +/// How deep a transitivity walk may go before it stops. +/// +/// A guard, not a tuning knob. A well-formed subsumption spine is acyclic and +/// shallow, but this crate runs on real harvested data where a cycle would +/// otherwise spin forever — and [`Closure::equivalence_cycles`] exists precisely +/// because cycles DO occur. The cap is reported by [`Closure::depth_cap`] so a +/// caller can tell "not entailed" from "we stopped looking", which are different +/// answers and must not be conflated. +pub const DEFAULT_DEPTH_CAP: usize = 64; + +/// The asserted subsumption graph, closed on demand. +/// +/// The closure is computed per query rather than materialised: a spine of N +/// classes has an O(N²) transitive closure but only O(N) asserted edges, and +/// almost every caller asks about a handful of classes. Materialising would +/// trade a cheap walk for an expensive table nobody reads in full. +#[derive(Debug, Clone, Default)] +pub struct Closure { + parents: HashMap>, + depth_cap: usize, +} + +impl Closure { + /// Build from asserted subsumptions. + /// + /// Duplicate assertions are kept as asserted — deduplicating here would + /// silently change what [`Self::asserted_len`] reports, and a caller + /// counting its own input has a right to get its own number back. + #[must_use] + pub fn from_asserted(edges: impl IntoIterator) -> Self { + let mut parents: HashMap> = HashMap::new(); + for e in edges { + parents.entry(e.sub).or_default().push(e.sup); + } + Self { + parents, + depth_cap: DEFAULT_DEPTH_CAP, + } + } + + /// Override the transitivity depth guard. + #[must_use] + pub fn with_depth_cap(mut self, cap: usize) -> Self { + self.depth_cap = cap; + self + } + + /// The depth guard in force — so a caller can distinguish "not entailed" + /// from "the walk stopped". + #[must_use] + pub const fn depth_cap(&self) -> usize { + self.depth_cap + } + + /// Number of asserted edges. + #[must_use] + pub fn asserted_len(&self) -> usize { + self.parents.values().map(Vec::len).sum() + } + + /// Whether any edge is asserted. + #[must_use] + pub fn is_empty(&self) -> bool { + self.parents.is_empty() + } + + /// Classes with at least one asserted superclass. + pub fn subclasses(&self) -> impl Iterator + '_ { + self.parents.keys().copied() + } + + /// **R1 + R2** — every superclass of `c`, transitively. + /// + /// Excludes `c` itself unless a cycle genuinely returns to it, which is the + /// signal [`Self::equivalence_cycles`] reads. Breadth-first, so the walk + /// terminates at `depth_cap` hops rather than at `depth_cap` nodes. + #[must_use] + pub fn supers_of(&self, c: ClassAddr) -> HashSet { + let mut seen = HashSet::new(); + let mut queue = VecDeque::from([(c, 0usize)]); + while let Some((node, depth)) = queue.pop_front() { + if depth >= self.depth_cap { + continue; + } + for &p in self.parents.get(&node).into_iter().flatten() { + if seen.insert(p) { + queue.push_back((p, depth + 1)); + } + } + } + seen + } + + /// **The first question: does `sub ⊑ sup` follow?** + /// + /// Reflexive per R1: every class subsumes itself, which is a fact even when + /// no edge is asserted for it. + #[must_use] + pub fn entails(&self, sub: ClassAddr, sup: ClassAddr) -> bool { + sub == sup || self.supers_of(sub).contains(&sup) + } + + /// Classes that reach themselves — an equivalence cycle. + /// + /// Empty for a sound spine. A non-empty result is not automatically a bug: + /// two classes an ontology models separately may be genuine synonyms. It IS + /// always a finding, because a cycle makes the two mutually substitutable, + /// and a consumer treating one as more specific than the other is then + /// relying on something the asserted set does not support. + #[must_use] + pub fn equivalence_cycles(&self) -> Vec { + let mut out: Vec = self + .parents + .keys() + .copied() + .filter(|&c| self.supers_of(c).contains(&c)) + .collect(); + out.sort_unstable(); + out + } +} + +/// What merging a set of axioms into an existing closure would do. +/// +/// Returned by [`Closure::merge`] **without mutating** the closure: a caller +/// decides whether to accept the merge after seeing the verdict, which is the +/// only order that makes the verdict useful. +#[derive(Debug, Clone, PartialEq, Eq, Default)] +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +pub struct MergeVerdict { + /// Axioms the closure already entailed. These corroborate the existing set + /// and add nothing — the strongest possible outcome for an axiom, and the + /// one that carries no risk. + pub corroborating: Vec, + /// Axioms the closure did NOT entail, and which introduce no cycle. New + /// structure the existing set was silent about — **enrichment**, not + /// conflict. Silence is not disagreement. + pub enriching: Vec, + /// Classes drawn into an equivalence cycle BY this merge. Empty means the + /// merge is sound over this fragment. + pub introduced_cycles: Vec, + /// Cycles that were already present before the merge — reported so the + /// merge cannot be blamed for them. + pub pre_existing_cycles: Vec, +} + +impl MergeVerdict { + /// Whether the merge introduces no new equivalence cycle. + /// + /// Note what this does NOT claim: soundness **over this fragment**. A merge + /// that is sound here can still be wrong under role composition or bottom + /// propagation, neither of which this crate implements. A caller needing + /// that guarantee needs a full reasoner, and the crate doc says where the + /// line is. + #[must_use] + pub fn is_sound(&self) -> bool { + self.introduced_cycles.is_empty() + } + + /// Total axioms considered. + #[must_use] + pub fn considered(&self) -> usize { + self.corroborating.len() + self.enriching.len() + } +} + +impl Closure { + /// **The second question: is adding `axioms` sound?** + /// + /// Splits them into corroborating and enriching, then closes the union and + /// reports any equivalence cycle the merge introduced. The receiver is + /// untouched; apply the merge yourself with [`Self::extended`] once the + /// verdict is acceptable. + #[must_use] + pub fn merge(&self, axioms: &[Subsumption]) -> MergeVerdict { + let pre: HashSet = self.equivalence_cycles().into_iter().collect(); + + let mut corroborating = Vec::new(); + let mut enriching = Vec::new(); + for &ax in axioms { + if self.entails(ax.sub, ax.sup) { + corroborating.push(ax); + } else { + enriching.push(ax); + } + } + + // Only the enriching axioms can change the closure, so only they are + // merged for the cycle check. Including the corroborating ones would + // cost a larger walk to reach an identical answer. + let merged = self.extended(&enriching); + let mut introduced: Vec = merged + .equivalence_cycles() + .into_iter() + .filter(|c| !pre.contains(c)) + .collect(); + introduced.sort_unstable(); + + let mut pre_existing: Vec = pre.into_iter().collect(); + pre_existing.sort_unstable(); + + MergeVerdict { + corroborating, + enriching, + introduced_cycles: introduced, + pre_existing_cycles: pre_existing, + } + } + + /// A copy with `axioms` added. Pairs with [`Self::merge`]: check first, + /// then extend. + #[must_use] + pub fn extended(&self, axioms: &[Subsumption]) -> Closure { + let mut parents = self.parents.clone(); + for ax in axioms { + parents.entry(ax.sub).or_default().push(ax.sup); + } + Closure { + parents, + depth_cap: self.depth_cap, + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + + const NS: u32 = 0x0301_0000; + + fn c(id: u32) -> ClassAddr { + ClassAddr::new(NS, id) + } + + fn sub(a: u32, b: u32) -> Subsumption { + Subsumption::new(c(a), c(b)) + } + + /// R1 + R2: transitivity derives what is not asserted, and reflexivity + /// holds for a class with no edges at all. + /// + /// The anti-vacuity half is `!entails(1, 9)`: without it, an `entails` that + /// returned `true` unconditionally would pass every positive assertion here. + #[test] + fn transitivity_derives_and_reflexivity_holds() { + let cl = Closure::from_asserted([sub(1, 2), sub(2, 3), sub(3, 4)]); + assert!(cl.entails(c(1), c(2)), "asserted"); + assert!(cl.entails(c(1), c(4)), "derived through two hops"); + assert!(cl.entails(c(7), c(7)), "reflexive even with no edges"); + assert!( + !cl.entails(c(1), c(9)), + "must NOT entail an unrelated class" + ); + assert!(!cl.entails(c(4), c(1)), "and must not run the wrong way"); + } + + /// The depth cap is a real limit and is REPORTED, so "not entailed" stays + /// distinguishable from "we stopped looking". + /// + /// Both directions are asserted: at cap 2 the far end is unreachable, at + /// the default it is reachable. A cap that did nothing would fail the first + /// assertion; one that clamped everything would fail the second. + #[test] + fn the_depth_cap_binds_and_is_visible() { + let chain: Vec = (1..10).map(|i| sub(i, i + 1)).collect(); + let shallow = Closure::from_asserted(chain.clone()).with_depth_cap(2); + assert_eq!(shallow.depth_cap(), 2); + assert!(!shallow.entails(c(1), c(10)), "beyond the cap"); + assert!(shallow.entails(c(1), c(3)), "within the cap"); + let deep = Closure::from_asserted(chain); + assert!(deep.entails(c(1), c(10)), "reachable at the default cap"); + } + + /// A sound spine has no cycles; a two-way assertion produces one. + /// + /// The can-stay-silent half uses a NON-trivial acyclic graph — an empty + /// closure would prove only that emptiness has no cycles. + #[test] + fn cycles_are_detected_and_absent_when_they_should_be() { + let acyclic = Closure::from_asserted([sub(1, 2), sub(2, 3), sub(1, 3), sub(4, 3)]); + assert!( + acyclic.equivalence_cycles().is_empty(), + "a real acyclic spine reports no cycle" + ); + let cyclic = Closure::from_asserted([sub(1, 2), sub(2, 1)]); + assert_eq!( + cyclic.equivalence_cycles(), + vec![c(1), c(2)], + "both ends of the equivalence are named" + ); + } + + /// A cycle closing through a LONG chain is still found — the property that + /// makes this a reasoner rather than a pairwise check. + #[test] + fn a_cycle_through_a_long_chain_is_found() { + let mut axioms: Vec = (1..8).map(|i| sub(i, i + 1)).collect(); + axioms.push(sub(8, 1)); // closes 1 → 8 → 1 + let cl = Closure::from_asserted(axioms); + assert_eq!(cl.equivalence_cycles().len(), 8, "every class on the ring"); + } + + /// **The merge verdict discriminates all three outcomes.** A verdict that + /// answered one class for everything would carry no information. + #[test] + fn merge_splits_corroborating_enriching_and_conflicting() { + let base = Closure::from_asserted([sub(1, 2), sub(2, 3)]); + + // Corroborating: already derivable through 1 ⊑ 2 ⊑ 3. + let v = base.merge(&[sub(1, 3)]); + assert_eq!(v.corroborating.len(), 1); + assert!(v.enriching.is_empty()); + assert!(v.is_sound()); + + // Enriching: the base is SILENT about 4, not opposed to it. + let v = base.merge(&[sub(4, 3)]); + assert!(v.corroborating.is_empty()); + assert_eq!(v.enriching.len(), 1); + assert!(v.is_sound(), "silence is not disagreement"); + + // Conflicting: the base says 1 ⊑ 3; the reverse closes a cycle. + let v = base.merge(&[sub(3, 1)]); + assert!(!v.is_sound(), "a direction conflict must NOT read as sound"); + assert_eq!(v.introduced_cycles, vec![c(1), c(2), c(3)]); + assert!(v.pre_existing_cycles.is_empty(), "the base was clean"); + } + + /// Pre-existing cycles are never blamed on the merge — the control that + /// makes `introduced_cycles` mean what it says. + #[test] + fn a_pre_existing_cycle_is_not_attributed_to_the_merge() { + let dirty = Closure::from_asserted([sub(1, 2), sub(2, 1)]); + let v = dirty.merge(&[sub(5, 6)]); + assert_eq!(v.pre_existing_cycles, vec![c(1), c(2)]); + assert!( + v.introduced_cycles.is_empty(), + "an innocent merge stays innocent against a dirty base" + ); + assert!(v.is_sound()); + } + + /// `merge` does not mutate; `extended` does. Checking first and applying + /// after is the only order in which a verdict is useful. + #[test] + fn merge_inspects_and_extended_applies() { + let base = Closure::from_asserted([sub(1, 2)]); + let before = base.asserted_len(); + let v = base.merge(&[sub(2, 3)]); + assert_eq!(base.asserted_len(), before, "merge left the closure alone"); + assert!(!base.entails(c(1), c(3))); + let applied = base.extended(&v.enriching); + assert!( + applied.entails(c(1), c(3)), + "and extended really applies it" + ); + } + + /// Addresses are class-scoped: the same identity under a different classid + /// is a different class, so no relation leaks across namespaces. + #[test] + fn identity_alone_does_not_make_two_classes_the_same() { + let other = 0x0302_0000; + let cl = Closure::from_asserted([Subsumption::new( + ClassAddr::new(NS, 1), + ClassAddr::new(NS, 2), + )]); + assert!(!cl.entails(ClassAddr::new(other, 1), ClassAddr::new(NS, 2))); + assert!(cl.entails(ClassAddr::new(NS, 1), ClassAddr::new(NS, 2))); + } +} diff --git a/docs/DISCOVERY-MAP.md b/docs/DISCOVERY-MAP.md index df69cf8..e1152ac 100644 --- a/docs/DISCOVERY-MAP.md +++ b/docs/DISCOVERY-MAP.md @@ -1768,3 +1768,33 @@ isolation. The map's job is to keep them visible. EXACTLY ONE), Klickwege wiring second (W2), PowerAutomate-shaped skin third (W3) — both skins Mario-editor ergonomics over `ClassView : WideFieldMask`, which is T1 applied at editor scale. + +- **D-ELK-FACTFINDER (`ogar-elk` — the EL subsumption closure as the third + factfinder; 2026-08-07; [G], CODED, operator-directed):** `ogar-obo` and + `ogar-ro` say what is **asserted**; nothing said what **follows**. + `ogar-elk` closes that gap with the smallest calculus that does the job — + three rules (R1 reflexivity, R2 transitivity, R3 merge-soundness) over + ABI-shaped `(classid, identity)` addresses. It answers exactly two + questions: does `A ⊑ B` follow, and is adding a set of axioms to an + existing closure sound. **Ungraded by construction** — an EL entailment is + a fact, so nothing here is scored, ranked or weighted; the thinking that + consumes these facts lives one layer out. **Addresses, never a file:** the + crate never parses an ontology, resolves a CURIE, or reads a label — + reasoning over the addressed form is the point of having addressed it. + **R3 is why this is a crate and not a transitive-closure helper:** two + independently authored sources can each be internally consistent and still + disagree about a relation's DIRECTION; merging then derives `A ⊑ B` and + `B ⊑ A` for classes neither calls equivalent, and that cycle — found at any + distance, including through chains no pairwise check would look at — is the + disagreement made mechanical. **Deliberate boundary, named in the crate + doc:** no existential restrictions, no role composition, no bottom + propagation, no conjunction/disjunction/complement. Each becomes necessary + the moment a typed cross-angle `ogar-ro` predicate enters the closure, and + at that point the correct move is to wrap a full reasoner (`whelk-rs`) — + not to grow the file. The hazard that boundary guards: without role + composition, walking subsumption and part-of together derives FALSE + ancestors (`A part_of B`, `B ⊑ C` does **not** give `A ⊑ C`), which is why + `Closure::from_asserted` takes a `Subsumption` type rather than raw pairs. + Zero-dependency, `forbid(unsafe_code)`, 8 tests each carrying the input + that would falsify it — depends: D-CLASSID-CANON-HIGH-FLIP (the address + form it consumes).