TransBox and mOWL: Closure and Tooling

📍 Where we are: Part III · Embedding Ontologies — Chapter 10. BoxEL and Box²EL made conjunction exact by trading balls for boxes; this chapter asks for the whole constructor set at once, defines what "closed under EL++" means, meets the model that proves a soundness theorem for it, and tours the toolkit that made all these experiments comparable.

Part II turned concepts into regions; the last two chapters trained balls, then boxes, each step repairing one operation. This chapter names the finish line. An ontology builds concepts by nesting intersection inside existential restriction to any depth, and a geometry that wants to be the ontology must supply a region for every such nested concept, assembled from the regions of its parts. That demand has a crisp name, EL++-closure, and a model that meets it, TransBox, whose central theorem is the geometric twin of Volume 2's model theory: if the training loss reaches exactly zero, the boxes are not an approximation of a model of the ontology, they are one [1]. The chapter closes with mOWL, the open-source library that standardized the pipeline (normalization, datasets, models, ranking evaluation) our companion files have been re-implementing in miniature all along [2].

The simple version

Imagine a workshop of machines that each take boards of one standard thickness and output boards of that same thickness. Because every output is a legal input, you can chain the machines forever. Now imagine one machine that outputs a curved shell instead: the chain breaks the moment you use it, because nothing downstream accepts a shell. A family of concept shapes is "closed" when every logical operation (overlap two shapes, look at a shape through a relation, chain two relations) hands back a shape of the same family, so any nested concept the ontology can write down is built by running the machines in sequence. Balls break the chain at the first overlap (a lens is not a ball). Boxes with one-arrow relations never output an illegal shape, but their relation machine has a sneakier defect: it pushes every board by the same fixed nudge, one destination per board, so a relation that must send one thing to many places, or obey several rules at once, has no slack to do it. TransBox rebuilds that machine with a whole range of allowed nudges, so the outputs stay boxes and the machine finally has room to serve every rule. And mOWL is the shared workshop itself: one set of jigs and gauges, so that when two labs claim their machines cut straighter, they measured with the same ruler.

What this chapter covers

The gap our probes left: we tested only atomic subsumptions between names, while real ontologies ask about complex concepts like Person ⊓ ∃authored.Paper; EL++-closure, defined precisely, is what it takes to answer those compositionally.
Why one translation per role fails: not by leaving the box family (a shifted box is still a box) but by collapsing capacity: the functional collapse (the TransE failure, replayed at the ontology level), the feasible-translation-set derivation, and the empty-intersection pathology our own code contains as an explicit vacuous branch.
TransBox's construction: a role becomes a box of translations, r(a, b) holds iff $x_a - x_b \in \mathrm{Box}(r)$ ; the Minkowski sum of two boxes is proved to be a box, and with it existential projection and role composition stay inside the family.
The soundness theorem: zero loss makes the geometry a model of the ontology, hence perfect recall on everything entailed; our two runs' real final losses, 0.6848 and 0.0678, quoted as the honest distance from that guarantee.
The evaluation the field runs: normalized-axiom and complex-axiom prediction on GALEN, the Gene Ontology, and Anatomy, and where the protocol echoes our kg.py filtered ranking.
mOWL as infrastructure: OWL (Web Ontology Language) in, jcel/ELK normalization behind a Java bridge, seven GCI buckets, one loss-dispatch contract across the model zoo, one rank-based evaluator; why shared tooling, not new losses, made results comparable.
A sober state-of-the-field table: ELEm, BoxEL, Box²EL, TransBox: region family, role mechanism, which constructors each serves with real capacity, and what each can prove.

The gap: we probed atoms, ontologies ask about molecules

Look honestly at what the last two chapters verified. The containment test sub_geo in el_embed.py (lines 301–305) and its box twin probe_gap in box_el.py (lines 381–389) are each scanned over the 56 ordered pairs of the 8 satisfiable named concepts, asking, for each pair, whether region A sits inside region B. Every question had the shape $A \sqsubseteq B$ where both $A$ and $B$ are atomic names: Professor ⊑ Researcher, Dean ⊑ Person. The symbol $\sqsubseteq$ is subsumption, "every instance of the left concept is an instance of the right one," exactly as in Volume 2.

Real ontologies do not stop at names. The EL++ concept language builds complex concepts from names using two constructors: conjunction $C \sqcap D$ ("both a C and a D") and existential restriction $\exists r.C$ ("something standing in relation r to at least one C"), nested to any depth. On the academic world, the concept "a person who authored at least one paper" is not a name in the TBox; it is the complex concept

\text{Person} \sqcap \exists \text{authored}.\text{Paper},

and a biomedical ontology asks queries of exactly this shape at industrial scale. A geometry that stores one region per name has no answer for such a question unless it can build the region of the complex concept from the regions of its parts. Volume 2's model theory satisfied that demand by definition. Read a superscript $\mathcal I$ as "the set of things the interpretation $\mathcal I$ assigns to this expression", and read $\cap$ as set intersection (the points lying in both sets), $\in$ as "is a member of", $\wedge$ as the logical "and", and $\{x : \ldots\}$ as "the set of all $x$ such that …": an interpretation assigns $(C \sqcap D)^{\mathcal I} = C^{\mathcal I} \cap D^{\mathcal I}$ and $(\exists r.C)^{\mathcal I} = \{x : \exists y.\ (x,y) \in r^{\mathcal I} \wedge y \in C^{\mathcal I}\}$ automatically, because sets are closed under every set operation. Regions of a fixed shape are not. That is the entire problem.

EL++-closure, precisely

Fix an embedding dimension, a whole number $d$ (the number of coordinates each point carries; our companion runs use $d = 8$ ), and let $\mathcal{F}$ be a family of subsets of $\mathbb{R}^d$ , the d-dimensional space of real vectors: the candidate concept regions. Let each role $r$ be interpreted as some binary relation $r^{\mathcal I} \subseteq \mathbb{R}^d \times \mathbb{R}^d$ , a set of ordered point pairs. Following the definition that TransBox makes central [1], call the pair (region family, role interpretations) EL++-closed when three conditions hold:

Closure under intersection. For all regions $R_1, R_2 \in \mathcal{F}$ , the set intersection $R_1 \cap R_2$ is again a member of $\mathcal{F}$ . This makes $C \sqcap D$ representable: its region is literally the intersection of the two parts' regions.
Closure under existential projection. For every role $r$ and every region $R \in \mathcal{F}$ , the existential projection $\exists r.R := \{x \in \mathbb{R}^d : \exists y \in R \text{ with } (x, y) \in r^{\mathcal I}\}$ , the set of points that see some point of $R$ through $r$ , is again a member of $\mathcal{F}$ .
Closure under role composition. For all roles $r, s$ , the composition $r^{\mathcal I} \circ s^{\mathcal I} := \{(x, z) : \exists y \text{ with } (x,y) \in r^{\mathcal I} \text{ and } (y,z) \in s^{\mathcal I}\}$ is again a relation the model can express with its role machinery, so that a chain axiom $r \circ s \sqsubseteq t$ becomes a checkable, trainable condition of the same kind as the others.

One bookkeeping note for readers who go to the source: the paper's full definition additionally requires $\mathcal{F}$ to contain the empty set (so ⊥ has a region), the whole space $\mathbb{R}^d$ (so ⊤ does), and every singleton $\{x\}$ (so an individual name does) [1]; we state here the three compositional conditions, because they are the ones that carry this chapter's argument. When all three hold, structural induction finishes the job: every EL++ concept, however deeply nested, gets a region in $\mathcal{F}$ . The base case is the names (each has its trained region); for the step, if $C$ and $D$ already have regions in $\mathcal{F}$ , condition 1 hands $C \sqcap D$ a region and condition 2 hands $\exists r.C$ one, both in $\mathcal{F}$ . No fresh training is required to answer a query about a concept never seen during training: closure turns an embedding from a lookup table over names into a calculator over concepts.

Score the Part's models against this definition. Balls fail condition 1: the previous chapters measured a 60.56 percent false-positive area when the lens-shaped intersection of two balls is replaced by its best enclosing ball (boxes_vs_balls.py, quoted in the box_el.py trace). Boxes pass condition 1 exactly, by the corner arithmetic $l_I = \max(l_A, l_B)$ , $u_I = \min(u_A, u_B)$ that box_el.py computes at lines 276–277. What about conditions 2 and 3 for the trained models, both of which interpret a role as a single translation vector $t_r$ ? Read purely as statements about shape, they pass too, and it is worth seeing why before seeing why that is not good enough. The single-translation role relation is $r^{\mathcal I} = \{(x, y) : y = x + t_r\}$ ; the existential projection of a box $R$ through it is $\{x : x + t_r \in R\} = R - t_r$ , the same box shifted, still a box; and the composition of two translation relations is the translation by $t_r + t_s$ , again a relation the same machinery expresses. The genuine defect is that this role interpretation is point-valued: the relation $y = x + t_r$ is a function, so every head has exactly one r-successor, the relation cannot be one-to-many, and one shared arrow has no freedom to serve several axioms at once. Useful closure therefore asks more of the roles than the three shape conditions alone: the role machinery must have the capacity to represent non-functional relations and to give every axiom that touches it room to hold. That capacity is what single translations lack and what TransBox restores by giving roles positive volume. We now derive the failure in detail.

Why a single translation per role fails: capacity, not shape

Volume 3 has met this failure once already, in vector form: TransE models a relation as one vector $\mathbf{w}_r$ with the score $\lVert \mathbf{e}_h + \mathbf{w}_r - \mathbf{e}_t \rVert$ , where $\mathbf{e}_h$ and $\mathbf{e}_t$ are the head and tail entities' vectors, $\mathbf{w}_r$ the relation's translation, and $\lVert\cdot\rVert$ (the norm bars) measures the length of the resulting mismatch vector, and a one-to-many relation forces distinct tails onto the same point. Replay the argument at the ontology level, where it bites three separate times.

First, the functional collapse on individuals. Suppose the geometry asserts $r(a, b)$ exactly when $x_b = x_a + t_r$ , with $x_a, x_b \in \mathbb{R}^d$ the entity points and $t_r \in \mathbb{R}^d$ the role's one translation. Let one head have two r-successors, $r(a, b)$ and $r(a, b')$ with $b \ne b'$ . Then both equations hold at once:

x_b = x_a + t_r, \qquad x_{b'} = x_a + t_r.

Subtract the second from the first. The right-hand sides are identical, so $x_b - x_{b'} = \mathbf{0}$ , which forces $x_b = x_{b'}$ : the two distinct successors collapse to one point. In the academic world, bob advises both carol and dave, so a strict single-translation reading of advises cannot even represent the knowledge graph's triples, let alone the TBox above them.

Second, the feasible-translation standoff on concepts. Our trained models soften the equation into containment hinges, so the collapse reappears as a constraint conflict rather than an equality. Take the box model. An NF3 axiom $A \sqsubseteq \exists r.B$ is trained as "box A, shifted by $t_r$ , sits inside box B" (box_el.py lines 226–241). Work out, axis by axis, which translations satisfy it exactly. Write $[l_{A,i},\, u_{A,i}]$ for box A's interval on axis $i$ (the index $i$ runs over the $d$ axes). The shifted box has interval $[l_{A,i} + t_i,\, u_{A,i} + t_i]$ , and containment in $[l_{B,i},\, u_{B,i}]$ demands both ends:

l_{B,i} \le l_{A,i} + t_i \quad\text{and}\quad u_{A,i} + t_i \le u_{B,i}.

Solve each inequality for $t_i$ : the first gives $t_i \ge l_{B,i} - l_{A,i}$ , the second gives $t_i \le u_{B,i} - u_{A,i}$ . So the translations satisfying this one axiom form, per axis, the interval

t_i \in \big[\, l_{B,i} - l_{A,i},\ u_{B,i} - u_{A,i} \,\big],

which is nonempty exactly when $u_{B,i} - u_{A,i} \ge l_{B,i} - l_{A,i}$ , i.e. when box B is at least as wide as box A on that axis. The feasible set for the whole axiom is thus itself a box of translations, and a role serving $k$ axioms must pick its single $t_r$ from the intersection of k such boxes. Nothing guarantees that intersection is nonempty even when the ontology is perfectly satisfiable: one arrow is being asked to map several differently placed, differently sized source boxes into their targets at once. The companion code documents the tug-of-war explicitly: the squared hinge was chosen because, with a plain L1 hinge, two opposing axioms "can cancel EXACTLY on a shared coordinate and stall while both stay active" as they pull one shared translation in opposite directions (box_el.py lines 181–184, the docstring of hinge_incl).

Third, composition pins the role to a single point. Chain two single-translation roles and the composed relation is again a translation, by $t_r + t_s$ : the shape survives (condition 3 is met, degenerately), but a chain axiom $r \circ r \sqsubseteq t$ now pins the target role's entire feasible set to a single point: the composed relation contains the pair $(x,\, x + 2\, t_r)$ for every $x$ , the axiom demands each such pair also lie in $t$ 's relation, so $x + 2\, t_r = x + t_t$ , and subtracting $x$ from both sides leaves $t_t = 2\, t_r$ , with no freedom at all. In the general case the target role also serves other axioms, each carving its own feasible box as derived above, and one hard-wired point must sit inside all of them at once; nothing guarantees it can. Our instance is the benign extreme that shows the other half of the story: the academic TBox's one chain, advises ∘ advises ⊑ grandAdvisor, happens to be grandAdvisor's only axiom, so hard-wiring $t_{\text{grandAdvisor}} = 2\, t_{\text{advises}}$ would satisfy it in isolation ("grandAdvisor's sole axiom is the skipped chain," notes el_embed.py at lines 86–87). The companions skip it anyway, for a plainer reason: the ELEm/ELBE training recipe compiles only the four normal forms plus disjointness into losses, so its vocabulary has no term for a role chain, and the axiom is dropped, not approximated (el_embed.py lines 13–16). Both companion modules refuse rather than pretend (box_el.py lines 56–62):

# The one role chain (advises ∘ advises ⊑ grandAdvisor) has no translation-only
# box encoding — it would need t_advises + t_advises to act like a third role —
# so it is skipped with a printed note, exactly as in el_embed.py.  (TransBox
# and Box²EL's bump machinery are the published fixes.)
CHAIN_AXIOMS: list[tuple] = [ax for ax in NORMALIZED if ax[0] == "chain"]
NF_AXIOMS: list[tuple] = [ax for ax in NORMALIZED
                          if ax[0] in ("nf1", "nf2", "nf3", "nf4")]

and the run announces it out loud, in the real committed output of python3 box_el.py:

   14 TBox axioms → 16 normal forms: 6 NF1 + 2 NF2 + 3 NF3 + 4 NF4 + 1 role chain
   skipped: advises ∘ advises ⊑ grandAdvisor — one translation vector cannot compose two hops

One normal form of sixteen, roughly six percent of the normalized ontology, is simply outside the language of everything we trained in the last two chapters. That is what the capacity failure looks like in practice: not a wrong answer but a question the training vocabulary cannot even pose.

A fourth, quieter pathology: intersections that die. There is one more trapdoor, and our own code contains it as an honest, explicit branch. When the trained boxes $A$ and $B$ fail to overlap on even one axis, their intersection is empty, and the conjunction axiom $A \sqcap B \sqsubseteq C$ is satisfied vacuously: the empty set is a subset of everything. box_el.py lines 308–312:

    # ORDINARY NF2 (A ⊓ B ⊑ C).  If the intersection is empty on some axis
    # (l_I > u_I), then A ⊓ B ≡ ⊥ and ∅ ⊑ C holds VACUOUSLY: loss 0, and the
    # subgradient is 0 (the axiom asks nothing of an empty intersection).
    if bool(np.any(lI > uI)):
        return 0.0, False

Logically this is correct, which is exactly what makes it dangerous as a learning signal: gradient descent can zero out a conjunction loss not by arranging the three boxes correctly but by shoving $A$ and $B$ apart until $A \sqcap B$ is empty. And raising the dimension makes this failure more likely, not less. Two boxes whose defining corners are drawn independently at random in $\mathbb{R}^d$ intersect with probability exactly $(2/3)^d$ : on each axis the four independent endpoint coordinates fall in one of the $4! = 24$ equally likely orders, the $2 \cdot 2! \cdot 2! = 8$ orders that place one interval entirely before the other make that axis miss, so a single axis overlaps with probability $1 - 8/24 = 2/3$ , and all $d$ independent axes must overlap at once. That probability collapses geometrically as $d$ grows; at $d = 50$ it is already under two in a billion, so in the high-dimensional spaces real ontologies are trained in, an empty intersection is the default outcome, not the exception [1]. TransBox's remedy for this pathology is a mechanism separate from its role boxes: it computes intersections as extended boxes whose per-axis components may individually be empty (coordinates drawn from $\mathbb{R} \cup \{\varnothing\}$ ), so an overlap that dies on one axis is recorded on that axis alone instead of annihilating the training signal of the whole region [1]. Closure under ⊓ is necessary but not sufficient; the intersections also have to stay alive, and keeping them alive takes machinery of its own.

TransBox's move: a role is a box of translations

Decoded first. The single-translation model says "relation r is the arrow $t_r$ ": one displacement, applied uniformly. TransBox says "relation r is a set of allowed arrows," and takes that set to be an axis-aligned box in the same space as the concepts. A pair of points stands in the relation whenever their displacement is one of the allowed arrows [1]:

r(a, b) \quad\text{holds iff}\quad x_a - x_b \in \mathrm{Box}(r),

where $x_a, x_b \in \mathbb{R}^d$ are the two points and $\mathrm{Box}(r) = \prod_{i=1}^{d} [\lambda_{r,i},\, \mu_{r,i}]$ is the role's box: the product of one interval per axis, with lower end $\lambda_{r,i}$ and upper end $\mu_{r,i}$ . The single translation is the degenerate case where every interval pinches to a point, so nothing is lost; what is gained is volume: a one-to-many role can hold between one head and many tails, because many displacements are allowed at once. (Our companion shifts the head by $+t_r$ , the point box containing $-t_r$ under this sign convention; the geometry is the same up to that reflection.)

The reason the enriched role keeps every constructor inside the box family is a small piece of geometry worth proving completely: the Minkowski sum of two axis-aligned boxes is an axis-aligned box. The Minkowski sum of two sets is the set of all pairwise sums, $P \oplus Q := \{p + q : p \in P,\ q \in Q\}$ . Because both boxes are products of intervals and addition acts coordinate by coordinate, it is enough to prove the one-dimensional case: $[l_1, u_1] \oplus [l_2, u_2] = [l_1 + l_2,\, u_1 + u_2]$ .

Containment left to right. Take any $y \in [l_1, u_1]$ and $z \in [l_2, u_2]$ . Adding the two chains of inequalities $l_1 \le y \le u_1$ and $l_2 \le z \le u_2$ termwise gives $l_1 + l_2 \le y + z \le u_1 + u_2$ , so every pairwise sum lands in the claimed interval.

Containment right to left. Take any target $w$ with $l_1 + l_2 \le w \le u_1 + u_2$ ; we must exhibit summands. Choose $y = \min(u_1,\, w - l_2)$ and $z = w - y$ . Check $y$ first: $y \le u_1$ by the definition of a minimum, and $y \ge l_1$ because both candidates are, $u_1 \ge l_1$ always, and $w - l_2 \ge l_1$ by rearranging the assumption $w \ge l_1 + l_2$ . Now check $z$ : from $y \le w - l_2$ we get $z = w - y \ge l_2$ ; and from $w \le u_1 + u_2$ we get $w - u_2 \le u_1$ , while $w - u_2 \le w - l_2$ holds because $l_2 \le u_2$ , so $w - u_2$ is at most both candidates for the minimum, hence $w - u_2 \le y$ , which rearranges to $z = w - y \le u_2$ . Both summands are legal, so every point of $[l_1+l_2,\, u_1+u_2]$ is attained. ∎

With this lemma, the three closure conditions fall in sequence.

Intersection was already closed for boxes: per axis, $[l_A, u_A] \cap [l_B, u_B] = [\max(l_A, l_B),\, \min(u_A, u_B)]$ , the corner arithmetic of the previous chapter, empty when some lower corner exceeds the corresponding upper corner.

Existential projection becomes a Minkowski sum. Unwind the definition and substitute $v = x - y$ :

\exists r.\mathrm{Box}(C) = \{x : \exists y \in \mathrm{Box}(C) \text{ with } x - y \in \mathrm{Box}(r)\} = \{y + v : y \in \mathrm{Box}(C),\ v \in \mathrm{Box}(r)\} = \mathrm{Box}(C) \oplus \mathrm{Box}(r),

which by the lemma is again a box, with corners computed by adding corners. On the academic world, take the complex concept ∃advises.Student, "everything that advises at least one student." Its region needs no training of its own; it is assembled symbolically from two trained objects:

\mathrm{Box}(\exists \text{advises}.\text{Student}) = \mathrm{Box}(\text{Student}) \oplus \mathrm{Box}(\text{advises}), \qquad l_i = l_{\text{Student},i} + \lambda_{\text{advises},i}, \quad u_i = u_{\text{Student},i} + \mu_{\text{advises},i},

and the TBox axiom Professor ⊑ ∃advises.Student becomes an ordinary box containment, $\mathrm{Box}(\text{Professor}) \subseteq \mathrm{Box}(\text{Student}) \oplus \mathrm{Box}(\text{advises})$ , checkable corner by corner with the same $2d$ inequalities as any NF1 axiom. Nest deeper and nothing new happens: Person ⊓ ∃authored.Paper is $\mathrm{Box}(\text{Person}) \cap (\mathrm{Box}(\text{Paper}) \oplus \mathrm{Box}(\text{authored}))$ , an intersection of two boxes, a box. Every constructor application is one round of corner arithmetic.

Composition stays inside the role family, and here the construction is exact, not an approximation. Suppose $r(x, y)$ and $s(y, z)$ , so $x - y \in \mathrm{Box}(r)$ and $y - z \in \mathrm{Box}(s)$ . Adding the two displacements telescopes:

x - z = (x - y) + (y - z) \in \mathrm{Box}(r) \oplus \mathrm{Box}(s).

Conversely, if $x - z = u + v$ with $u \in \mathrm{Box}(r)$ and $v \in \mathrm{Box}(s)$ , set the witness $y = x - u$ ; then $x - y = u \in \mathrm{Box}(r)$ and $y - z = (x - z) - u = v \in \mathrm{Box}(s)$ , and since the domain is all of $\mathbb{R}^d$ , the witness always exists. So the composed relation is exactly the relation of the box $\mathrm{Box}(r) \oplus \mathrm{Box}(s)$ , and the chain axiom our companions had to skip becomes one more trainable containment between boxes:

\text{advises} \circ \text{advises} \sqsubseteq \text{grandAdvisor} \quad\Longleftrightarrow\quad \mathrm{Box}(\text{advises}) \oplus \mathrm{Box}(\text{advises}) \subseteq \mathrm{Box}(\text{grandAdvisor}),

per axis $2\lambda_{\text{advises},i} \ge \lambda_{\text{grand},i}$ and $2\mu_{\text{advises},i} \le \mu_{\text{grand},i}$ . The sixteenth normal form, the one both our runs printed a skip notice for, is no longer outside the language. Boxes for concepts, boxes for roles, and the three constructors all reduce to max, min, and plus on corners: the family is EL++-closed, and this time with roles of positive volume, so the closure carries real capacity instead of collapsing to points [1].

EL++-closure in pictures: intersection, existential projection, and role composition all stay inside the box family once a role is a box of translations, while the mOWL pipeline underneath standardizes how any such model is normalized, trained, and ranked. Original diagram by the authors, created with AI assistance.

The soundness theorem, and our honest distance from it

The construction supports a theorem with real logical content. TransBox attaches to each normalized axiom a loss term that equals zero exactly when the corresponding geometric condition holds (containment for subsumptions, an empty overlap for disjointness, Minkowski containment for chains), and proves the following [1]:

Soundness. If the total training loss over the normalized ontology is exactly zero, then the geometric interpretation, domain $\mathbb{R}^d$ , each concept name mapped to its box, each role mapped to the relation $\{(x,y) : x - y \in \mathrm{Box}(r)\}$ , with complex concepts interpreted by the corner arithmetic above, is a model of the ontology: every axiom is true in it.

Pause on what that buys. In Volume 2, an ontology $\mathcal{O}$ entails a statement $\varphi$ , written $\mathcal{O} \models \varphi$ , when $\varphi$ is true in every model of $\mathcal{O}$ . Apply the definition to a zero-loss geometry: it is a model, so every entailed statement is true in it in particular. If $\mathcal{O} \models A \sqsubseteq B$ , then $\mathrm{Box}(A) \subseteq \mathrm{Box}(B)$ , with no tolerance parameter and no exceptions. A zero-loss geometry therefore has perfect recall on entailments: it cannot geometrically deny anything the logic proves. What it does not have is perfect precision. A model is one world among many, and one world may make extra statements true that the ontology does not entail (our geometry might place every Dean inside Topic by accident of initialization). Soundness-by-zero-loss bounds the errors on one side only, and that asymmetry is the honest shape of the guarantee.

Now the uncomfortable question the theorem forces on us: did our runs earn it? Neither did, and the committed numbers say so precisely. The ball model's real training trace (python3 el_embed.py):

training: full-batch loss (per-form pieces; epoch 1 = untrained)
  epoch :    total     nf1     nf2     nf3     nf4    disj     reg
      1 :  15.3500  7.4906  1.7265  3.7316  2.4013  0.0000  0.0000
    100 :   0.8361  0.3984  0.0000  0.3518  0.0000  0.0461  0.0398
   1000 :   0.6078  0.1239  0.0000  0.0659  0.0000  0.4168  0.0011
   3000 :   0.6848  0.1286  0.0000  0.0615  0.0000  0.4943  0.0004
  (the loss cannot reach 0: no geometry satisfies TenuredStudent ⊑
   Professor and ⊑ Student while the two stay γ_d apart — the
   unsatisfiable concepts keep an irreducible residual.)

and the box model's (python3 box_el.py):

   epoch :      total |      NF1     NF2⊓     disj      NF3      NF4
       1 :   283.4835 | 121.3894   0.0000   0.0000  62.7180  99.3761
:    10.3909 |   6.2613   0.0000   0.0002   1.9388   2.1907
:     1.1293 |   0.3796   0.4096   0.0000   0.2306   0.1095
:     0.2988 |   0.1469   0.0257   0.0000   0.1068   0.0193
:     0.1465 |   0.0800   0.0174   0.0000   0.0488   0.0003
:     0.0943 |   0.0510   0.0149   0.0000   0.0284   0.0000
:     0.0804 |   0.0425   0.0150   0.0000   0.0228   0.0000
:     0.0678 |   0.0351   0.0150   0.0031   0.0146   0.0000

Read the traces against the theorem. The ball run falls to 0.6078 at the epoch-1000 snapshot and then rises to 0.6848 by epoch 3000; the growing disj column shows the disjointness hinge and the two containment hinges of the unsatisfiable TenuredStudent locked in a spring equilibrium. The box run does far better, 283.4835 down to 0.0678, three and a half orders of magnitude, but the floor is not zero, and part of the reason is structural: both parameterizations give every concept a region of strictly positive volume, so ⊥ is not representable, and any geometry that must host TenuredStudent inside two disjoint boxes carries a permanent violation. (A genuine logical model would simply set $\text{TenuredStudent}^{\mathcal I} = \varnothing$ ; a positive-volume box cannot.) So the theorem's hypothesis fails for both runs, and everything we know about our trained geometries comes instead from the theorem's empirical shadow, the soundness probe. There the news is good, and real:

4. soundness probe — accept A ⊑ B iff gap(A,B) = max_i max(l_B−l_A, u_A−u_B) ≤ ε = 0.05
   the 8 gold subsumptions, by their trained gaps:
     Dean       ⊑ Person      gap = -0.1048  ✓ contained
     Dean       ⊑ Professor   gap =  0.0199  ✓ contained
     Dean       ⊑ Researcher  gap = -0.0544  ✓ contained
     Professor  ⊑ Person      gap = -0.1000  ✓ contained
     Professor  ⊑ Researcher  gap = -0.0500  ✓ contained
     Researcher ⊑ Person      gap =  0.0000  ✓ contained
     Student    ⊑ Person      gap = -0.0500  ✓ contained
     Student    ⊑ Researcher  gap = -0.0500  ✓ contained
   scan of 8·7 = 56 ordered pairs: predicted 8, TP 8, FP 0, FN 0

Eight of eight gold subsumptions contained, zero spurious containments. But notice what the probe conceded that the theorem would not: a tolerance at all. Dean ⊑ Professor holds only with a positive gap of 0.0199, a genuine protrusion forgiven because it is under $\varepsilon = 0.05$ . Perfect probe scores at nonzero loss are evidence, not proof; the theorem is the contract our miniature runs approach but do not sign. The two summary lines, verbatim from the committed runs, are this Part's empirical bottom line:

SUMMARY el_embed: trained_axioms=15 skipped_chains=1 gold=8 tp=8 fp=0 fn=0 precision=1.0000 recall=1.0000 final_loss=0.6848 disjoint_gap=0.1117
SUMMARY box_el: gold=8/8 tp=8 fp=0 fn=0 precision=1.0000 recall=1.0000 ball_recall=1.0000 final_loss=0.0678 min_overlap=-0.0304

The evaluation the field actually runs

Our 56-pair probe is a miniature of the field's standard protocol, which comes in two tiers [1][3]:

Normalized-axiom prediction. Hold out a slice of the ontology's normalized axioms, train on the rest, and treat each held-out axiom as a ranking query: for $A \sqsubseteq\ ?$ , score every concept name as a candidate right-hand side by the model's geometric containment score, sort, and record the rank of the true answer. Ranks aggregate into Mean Reciprocal Rank (MRR, the average of 1/rank) and Hits@k (the fraction of queries ranked at most k), under the filtered convention that candidates forming a different known-true axiom are removed before counting. This is, item for item, the protocol our kg.py implements for triples: rank_of (lines 79–104) scores every candidate, filters known-true corruptions, and counts survivors ranked strictly higher; evaluate (lines 110–122) folds the ranks into filtered MRR and Hits@1/3/10 over head and tail corruption. Reading a GALEN subsumption-prediction table and reading our six-query link-prediction table is the same skill.

Complex-axiom prediction. The stronger test, the one closure exists to serve: hold out subsumptions $C \sqsubseteq D$ where $C$ or $D$ nests ⊓ and ∃. Because ontologies rarely assert such axioms directly, the held-out set is generated symbolically: TransBox's evaluation uses LETHE, a uniform-interpolation ("forgetting") engine that eliminates chosen names from the ontology and, in doing so, manufactures entailed axioms with genuinely complex sides [1]. A model that stores only per-name regions must construct the region of each complex side before it can rank anything, exactly the ability EL++-closure grants and non-closed models must approximate. The standard corpora for both tiers are GALEN (a clinical-terminology ontology), the Gene Ontology, and Anatomy, the biomedical scale that motivated EL++'s polynomial design in Volume 2. On these, the reported result is a trade-off, not a sweep: TransBox's decisive wins are on the complex tier, exactly where closure is the whole game, while on plain normalized axioms it generally ranks behind the non-closed Box²EL and the ball baselines, a cost the paper reports itself [1]. We quote the shape of that finding, not its digits: the numbers belong to their paper's tables, and our own committed numbers are the ones this chapter stands behind.

mOWL: the toolkit that made the results comparable

Every model in this Part consumed the same four normal forms, trained on hinges, and was judged by ranks. That uniformity is not a law of nature; it is infrastructure. mOWL (machine learning with OWL) is a Python library that packages the entire ontology-embedding pipeline behind one interface [2], and walking its stages shows why the field's results became comparable at all.

OWL in. The input is a real ontology file in the OWL standard, SNOMED-scale if need be, not a hand-typed axiom list. Because the reference OWL machinery (the OWL API, the reasoners) lives on the Java Virtual Machine, mOWL reaches it through JPype, a Python-to-Java bridge; the Python user never sees the JVM directly.

Normalization behind the bridge. The jcel reasoner's normalization pass, with ELK available for reasoning at scale, rewrites the ontology into EL's normal forms, the role Volume 2's normalize played for our 14 axioms. The output is bucketed into seven GCI datasets (GCI, general concept inclusion, the umbrella term for axioms $C \sqsubseteq D$ ): the four satisfiable shapes $A \sqsubseteq B$ , $A \sqcap B \sqsubseteq C$ , $A \sqsubseteq \exists r.B$ , $\exists r.B \sqsubseteq A$ , plus the three bottom variants $A \sqsubseteq \bot$ , $A \sqcap B \sqsubseteq \bot$ , and $\exists r.B \sqsubseteq \bot$ . Our companion's split of NF2 into "ordinary" and "disjointness" branches (box_el.py lines 308–322 versus 281–306) is a two-bucket shadow of the same idea: ⊥-right axioms need different geometry, so they get their own bucket.

One loss-dispatch contract. Each embedding model is an ELModule implementing one loss method per GCI bucket; training iterates the buckets and dispatches. Under that single contract mOWL ships the zoo this Part has climbed: ELEm (the balls of the EL Embeddings chapter), ELBE (boxes with single-translation roles: our box_el.py, whose docstring says "BoxEL-style" for its box parameterization, trains exactly ELBE's translation roles; the two box lineages are untangled in BoxEL and Box²EL), BoxEL, and Box²EL with its bump vectors [2][3]. Swapping models changes one class name, not the experiment; TransBox itself was evaluated on a re-implementation of the Box²EL setup (with a corrected evaluation), the same dividend one layer up [1].

One evaluator. A RankBasedEvaluator runs the filtered ranking protocol against whichever model is plugged in, so a reported MRR means the same thing across papers sharing the harness. The library also carries the graph-projection alternative, OWL2Vec*, which walks a graph rendering of the ontology and embeds it with word-vector machinery instead of geometric losses: the region-based family of this Part is one wing of a larger ecosystem sharing the same inputs and evaluators [4].

The claim worth italicizing: the decisive contribution here was not any single loss function, it was shared tooling. Before a common harness, every paper normalized, split, and filtered differently, and the numbers could not be laid side by side; after it, an improvement had to survive on identical data through an identical evaluator. Our companion suite is deliberately mOWL-in-miniature, so this pipeline is something you have already run end to end:

mOWL stage	what it does	our miniature
OWL ingestion (JPype)	load a real ontology	`ontology.py` (the 14-axiom TBox)
jcel/ELK normalization	rewrite into GCI buckets	`el_completion.normalize` (16 normal forms)
seven GCI buckets	one dataset per axiom shape	NF1–NF4 lists plus the `disj` branch
ELModule zoo	one loss per bucket, per model	`el_embed.py` (balls), `box_el.py` (boxes)
RankBasedEvaluator	filtered MRR / Hits@k	`kg.py` `evaluate` (lines 110–122); the 56-pair probes

The state of the field, in one sober table

Part III began with hand-placed regions and ends here. One table summarizes what each trained model of this arc represents, what it is closed under, and what it can prove [1][3]:

model	concept regions	roles	constructors served (shape and capacity)	soundness story
ELEm	open balls	one translation vector	⊓ leaves the family (a lens is not a ball); roles point-valued	none; probes only
BoxEL	axis-aligned boxes	affine maps per role	⊓ exact; the role map keeps box shapes but is deterministic, so no one-to-many capacity and no room for chains	volume-based semantics for facts; proves its own zero-loss theorem (loss 0 ⟹ a model), but its point-valued roles leave complex-concept and chain queries out of reach
Box²EL	boxes plus per-concept bump vectors	head/tail boxes with bumps	⊓ exact; bumps buy relational capacity, but no compositional region for a nested ∃ or a chain	proves its own zero-loss theorem too (loss 0 with margin γ ≤ 0 ⟹ a model), the same shape as BoxEL/TransBox, but the guarantee does not reach the complex-concept and closure queries TransBox's does; strong empirical ranking [3]
TransBox	axis-aligned boxes	a box of translations per role	⊓, ∃-projection, ∘, all exact and with role volume (EL++-closed, with capacity)	theorem: zero loss ⟹ the geometry is a model, for the full constructor set [1]

Read the last two columns together and the Part's arc is visible in miniature. The zero-loss idea is not TransBox's invention: both BoxEL and Box²EL proved theorems of the same shape first. What grew is the reach of the theorem, from a construction exact for ⊓ alone to one that serves every constructor the language has, with roles wide enough to carry it, so that "zero loss makes a model" finally covers the complex concepts and chains an ontology actually asks about. That limit is an idealization (our best run stopped at 0.0678), but it is the right one, because it makes the embedding answerable to Volume 2's standard of correctness rather than to leaderboard intuition.

The unsolved part

Every theorem in this chapter lives in flat Euclidean space, and flat space is quietly the wrong shape for the thing being embedded. The gold structure of the academic world, of GALEN, of the Gene Ontology, is a hierarchy: Person above Researcher above Professor above Dean, a tree that widens as it descends. A tree with branching factor $b$ has $b^k$ nodes at depth $k$ , exponential growth, while the volume inside a Euclidean ball of radius $k$ grows only polynomially in $k$ for any fixed dimension $d$ . Something has to give: either the dimension climbs with the hierarchy, or the embedding pays distortion, siblings crushed together, cousins pulled spuriously close, the price growing with depth. Closure and soundness say nothing about this cost; they are statements about representability at zero loss, not about how much geometric room the optimizer has on the way down, and our runs' stubborn residuals, 0.6848 and 0.0678, are partly the sound of axioms competing for room in a space that grants it polynomially. Whether the closure-and-soundness program can be rebuilt in a geometry whose volume grows as fast as the trees it must hold, and what corner arithmetic even means there, is genuinely open. The next chapter takes the first step by changing the space itself.

Why it matters

This chapter is the hinge between representation and the integration volume ahead. Volume 4's project, making logic differentiable, needs exactly the two commodities established here. First, compositional geometry: a semantic loss or a differentiable query engine must build the score of a complex formula from the scores of its parts, and EL++-closure is the region-level statement of that requirement. Second, a soundness contract: "zero loss implies a model" is the template for the guarantees Volumes 4 and 5 keep reaching for, the point where a learned object stops being judged by test accuracy and starts being judged by model theory. The gap our runs exposed, guarantees that hold only at a zero the optimizer never reaches, is equally load-bearing: it is the honest form of "when can you trust a trained reasoner," and it returns, sharpened, in Volume 5's faithfulness chapters. And the mOWL lesson, that shared harnesses precede shared progress, is the methodological spine of every capstone in this series.

Key terms

Complex concept — a concept built from names by conjunction (⊓) and existential restriction (∃r.C), such as Person ⊓ ∃authored.Paper.
EL++-closure — a family of concept regions (with its role interpretations) closed under intersection, existential projection, and role composition, so every complex concept gets a region built from its parts' regions; useful only when the roles also carry the capacity (positive volume) to represent one-to-many relations.
Existential projection — the region $\{x : \exists y \in R,\ (x,y) \in r^{\mathcal I}\}$ of points seeing some point of region $R$ through role $r$ ; for TransBox it equals $R \oplus \mathrm{Box}(r)$ .
Minkowski sum (⊕) — the set of all pairwise sums of two sets; for axis-aligned boxes it is again a box, with corners $l_1 + l_2$ and $u_1 + u_2$ per axis.
Role box — TransBox's interpretation of a role: an axis-aligned box of allowed translations, $r(a,b)$ iff $x_a - x_b \in \mathrm{Box}(r)$ ; a single translation is the degenerate point box.
Soundness theorem (zero-loss model) — a geometry with exactly zero training loss is a model of the ontology, hence satisfies every entailed statement: perfect recall, not perfect precision.
Normalized-axiom / complex-axiom prediction — the field's two ranking evaluations: held-out normal-form axioms ranked by geometric score, and held-out LETHE-generated subsumptions with complex sides.
GCI (general concept inclusion) — an axiom $C \sqsubseteq D$ ; mOWL buckets a normalized ontology into seven GCI datasets (four satisfiable shapes, three ⊥-right variants).
mOWL — the Python library standardizing the pipeline: OWL ingestion over JPype, jcel/ELK normalization, the ELModule zoo under one loss-dispatch contract, a shared rank-based evaluator.

Where this leads

The unsolved part named the enemy precisely: hierarchies grow exponentially and flat space does not. The next chapter, Hyperbolic Embeddings, stops fighting the space and replaces it: in the Poincaré ball, volume grows exponentially with radius, at the same rate as the trees we keep trying to embed. There we derive the hyperbolic distance and its Riemannian gradient, and run a two-dimensional head-to-head in which the curved space beats the flat one on the academic hierarchy at an identical parameter budget, the hierarchy read straight off each point's distance from the origin.

Companion code: examples/neural/box_el.py (boxes, corner arithmetic, the vacuous-intersection branch, the 56-pair probe) and examples/neural/el_embed.py (balls, the single-translation hinges, the irreducible residual) produce every number quoted in this chapter; python3 box_el.py reruns both, byte-identically, and examples/neural/kg.py supplies the filtered-ranking evaluator the field-scale protocols mirror.

What this chapter covers​

The gap: we probed atoms, ontologies ask about molecules​

EL++-closure, precisely​

Why a single translation per role fails: capacity, not shape​

TransBox's move: a role is a box of translations​

The soundness theorem, and our honest distance from it​

The evaluation the field actually runs​

mOWL: the toolkit that made the results comparable​

The state of the field, in one sober table​

The unsolved part​

Why it matters​

Key terms​

Where this leads​