EL Embeddings: Geometry Meets Logic

📍 Where we are: Part III · Embedding Ontologies — Chapter 8. Boxes versus Balls placed its regions by hand and proved what each shape can carve; this chapter hands the placement to gradient descent, trains balls against Volume 2's real TBox, and then audits the trained geometry against Volume 2's own reasoner.

Part II ended with a prediction: balls cannot represent conjunction exactly, so a ball-based rendering of an ontology must bend somewhere. This chapter runs the experiment that prediction was filed against. The method is ELEm (EL Embeddings), a construction that maps every concept of an EL++ TBox (the terminological box: an ontology's schema-level axioms, written here in EL++, the lightweight description logic whose reasoner Volume 2 built) to an 8-dimensional ball and every role to a translation vector, then turns each normalized axiom into a differentiable penalty, so that gradient descent literally tries to build a geometric model of the ontology [1]. Everything here is a controlled experiment on the academic world: the same 14 axioms Volume 2 classified, pushed through the same normalize() function, trained with hand-written gradients, and scored against the completion algorithm's own verdict. The score at the end is a confusion table, not an impression.

The simple version

Imagine a law book for a city of circular zoning districts. Each law is a shape constraint: "the Professor district must lie entirely inside the Researcher district," "the Professor and Student districts may not overlap," "shifting the Professor district two blocks east must land it inside the Student district." A planner throws circles down at random, then nudges each one, day after day, in whatever direction reduces the total violation of all the laws at once. After three thousand days the map looks lawful, but "looks lawful" is not a certificate. So an inspector walks the map with a ruler and checks every pair of districts: does it assert containments the law book never demanded, and does it miss ones the law book entails? The planner is gradient descent, the map is the embedding, and the inspector is Volume 2's reasoner. This chapter is the inspector's report.

What this chapter covers

• The controlled setup: the same TBox, the same normalization (14 axioms → 16 normal forms, recomputed by importing Volume 2's own code), and Volume 2's classification as the gold standard; nothing retyped, nothing invented.
• Concepts as balls, roles as translations: the parameter blocks $c_A \in \mathbb{R}^8$, $r_A = e^{\rho_A}$, $v_r \in \mathbb{R}^8$, and a full derivation of the containment criterion $\lVert c_A - c_B \rVert + r_A \le r_B$ that everything else builds on.
• Five hinges from four normal forms plus disjointness: each loss derived from its axiom shape with its subgradient worked out, including why the existential's side flips the radius signs, why the conjunction loss is the awkward one, and why disjointness is where balls are natural.
• What zero loss would mean: the NF1 and NF3 hinges vanish exactly when their axioms hold, the disjointness hinge only once the balls also clear an extra safety margin (so its zero still guarantees the axiom), but the NF4 and NF2 hinges are strictly weaker than theirs, so even loss 0 would not certify a model, and even a model would guarantee only recall, never precision; a three-line triangle-inequality argument proves our TBox forbids zero loss anyway.
• The committed training trace: the loss falling 15.3500 → 0.8361 → 0.6078 and then rising to 0.6848, the skipped role chain printed out loud, and the trained radii recovering the concept hierarchy by size.
• The soundness probe: the geometric subsumption test with its slack $\varepsilon$, scored over all 56 ordered pairs of satisfiable named concepts: TP 8, FP 0, FN 0, precision and recall 1.0000 on this tiny TBox, and why scale changes that picture.
• Where the analogy frays: what the geometry does with the two concepts Volume 2 proved unsatisfiable, in a space that has no ball for ⊥.

The controlled experiment: same axioms, same normal forms, same gold

An experiment about whether geometry respects logic is worthless if the geometry and the logic quietly disagree about what the axioms are. So the companion module el_embed.py refuses to retype anything. Its first working lines import the ontology and the reasoner of Volume 2 directly (el_embed.py lines 37–40):

import kg  # noqa: F401  — wires sys.path to ../logic and ../symbolic
import ontology as onto
from ontology import BOT, TOP
from el_completion import normalize, classify

Three reused artifacts pin the experiment down. First, the axioms: onto.TBOX is the same 14-axiom EL++ TBox that every Volume 2 chapter traced (ontology.py lines 125–174). Second, the normal forms: the call NORMALIZED, FRESH_NAMES = normalize(onto.TBOX) (el_embed.py line 62) runs Volume 2's own normalization (el_completion.py lines 69–154), which returns 16 normal-form axioms in the four flat shapes the EL++ machinery is built on [2], plus the two fresh names _N1, _N2 it invented along the way. Exactly one of the 16 is the role chain advises ∘ advises ⊑ grandAdvisor; the other 15 are split off as TRAINABLE (el_embed.py lines 63–64) and will each become one loss term. Third, the gold standard: classify() (el_completion.py lines 302–319) reruns the completion algorithm to its fixpoint, and el_embed.py lines 121–126 read off the answer — 8 subsumptions between the 8 satisfiable named concepts, and 2 unsatisfiable concepts. The committed run prints the whole contract:

normalization — Volume 2's normalize(), recomputed, never retyped
  14 TBox axioms → 16 normal-form axioms
  trained  : 6 nf1 + 1 nf2 (⊓) + 3 nf3 + 4 nf4 + 1 disjointness (⊑ ⊥) = 15 loss terms
  SKIPPED  : advises ∘ advises ⊑ grandAdvisor — ELEm's loss vocabulary has no
             term for a role chain: the axiom is dropped, not approximated.
  ⊥ gets no ball: Professor ⊓ Student ⊑ ⊥ trains only the
             disjointness hinge that pushes the two balls apart.

gold standard — Volume 2's classify(), recomputed
  8 subsumptions between the 8 satisfiable named concepts:
    Dean ⊑ Person, Professor, Researcher
    Professor ⊑ Person, Researcher
    Researcher ⊑ Person
    Student ⊑ Person, Researcher
  2 unsatisfiable concepts (no consistent ball exists —
    excluded from the probe): TenuredStudent, TenuredStudentAdvisor

Notice what the SKIPPED line concedes before training even starts. The gap is definitional: ELEm's loss vocabulary compiles exactly the four normal forms plus disjointness, and it contains no term for a role chain, so "an advises edge followed by an advises edge implies a grandAdvisor edge" is dropped, not approximated. The translation reading could in principle accommodate the chain, since composing two advises steps translates a point by $2\,v_{\text{advises}}$, so setting $v_{\text{grandAdvisor}} = 2\,v_{\text{advises}}$ (say, by a hinge on $\lVert v_{\text{advises}} + v_{\text{advises}} - v_{\text{grandAdvisor}} \rVert$) would encode it; the published recipe simply never asks. So grandAdvisor gets no vector, the axiom leaves no trace on the geometry, and the module says so out loud and asserts the count (el_embed.py lines 350–354): 16 normal forms in, exactly 1 chain excluded, exactly 15 compiled into losses. That expressive gap is the first entry in the honest ledger this chapter keeps. Other ontology-embedding systems dodge such questions by treating axioms as text: Onto2Vec feeds axiom strings to a word-embedding model [3], and OWL2Vec* walks the ontology's graph projection [4]; neither offers any geometric statement that an axiom holds. ELEm's whole point is that the geometry makes such a statement, which is exactly what makes it checkable [1].

Concepts as balls, roles as translations

Now the formal setup, notation first. The embedding dimension $d$ is the number of coordinates each point carries; here $d = 8$ (el_embed.py line 44). Every concept $A$ that survives into a trainable axiom receives two parameters: a center $c_A \in \mathbb{R}^8$, a list of eight real numbers locating the concept in space, and a radius $r_A$, a single positive number giving its extent. The concept's region is the ball

$$B(c_A, r_A) \;=\; \lbrace\, x \in \mathbb{R}^8 : \lVert x - c_A \rVert \le r_A \,\rbrace,$$

where $\lVert \cdot \rVert$ is the Euclidean norm, the square root of the sum of squared components. The radius is stored as a log-radius $\rho_A$ with $r_A = e^{\rho_A}$, so that $r_A$ stays positive no matter what gradient descent does to $\rho_A$; by the chain rule, any derivative with respect to $r_A$ converts to one with respect to $\rho_A$ via $\frac{\partial L}{\partial \rho_A} = \frac{\partial L}{\partial r_A} \cdot \frac{d r_A}{d \rho_A} = \frac{\partial L}{\partial r_A} \cdot e^{\rho_A} = \frac{\partial L}{\partial r_A} \cdot r_A$ (el_embed.py lines 137–142). Every role $r$ used by a trainable axiom receives a translation vector $v_r \in \mathbb{R}^8$, the same device TransE used for knowledge-graph relations, now recruited for existential restrictions. Thirteen concepts get balls: the 10 declared names, the fresh _N1 and _N2, and ⊤, the top concept that contains every individual (it occurs as the filler, the concept written after the dot, in Volume 2's axiom ∃advises.⊤ ⊑ Researcher; the symbol $\exists$ reads "there exists", the existential restriction $\exists r.B$ names everything with an $r$-edge to at least one member of $B$, and the axiom says anyone who advises anything at all is a researcher). ⊥ deliberately gets none, and only two roles, advises and authored, get vectors; grandAdvisor's sole axiom is the skipped chain, so it gets nothing (el_embed.py lines 84–90).

Everything in this chapter rests on one geometric fact, so we derive it in full: ball containment has a closed-form criterion,

$$B(c_A, r_A) \subseteq B(c_B, r_B) \quad\Longleftrightarrow\quad \lVert c_A - c_B \rVert + r_A \;\le\; r_B .$$

Criterion implies containment. Take any point $x$ of ball $A$, so $\lVert x - c_A \rVert \le r_A$. The triangle inequality (the direct distance between two points is at most the distance through a third) gives

$$\lVert x - c_B \rVert \;\le\; \lVert x - c_A \rVert + \lVert c_A - c_B \rVert \;\le\; r_A + \lVert c_A - c_B \rVert \;\le\; r_B,$$

the last step by the criterion. So $x$ lies in ball $B$, and since $x$ was arbitrary, all of ball $A$ does.

Containment implies criterion. Suppose ball $A$ sits inside ball $B$ and consider the point of ball $A$ farthest from $c_B$: walk from $c_A$ directly away from $c_B$ for a distance $r_A$. Formally, let $u = (c_A - c_B) / \lVert c_A - c_B \rVert$ be the unit vector from $c_B$ toward $c_A$ (if the centers coincide, any unit vector works), and set $x^\ast = c_A + r_A u$. This point belongs to ball $A$ because $\lVert x^\ast - c_A \rVert = \lVert r_A u \rVert = r_A$. Its distance to $c_B$ computes exactly: $c_A - c_B$ equals $\lVert c_A - c_B \rVert \, u$, so

$$\lVert x^\ast - c_B \rVert \;=\; \big\lVert (c_A - c_B) + r_A u \big\rVert \;=\; \big\lVert \big(\lVert c_A - c_B \rVert + r_A\big)\, u \big\rVert \;=\; \lVert c_A - c_B \rVert + r_A,$$

because both summands point along the same unit vector $u$ and lengths of parallel vectors add. Containment forces $x^\ast$ into ball $B$, so $\lVert c_A - c_B \rVert + r_A \le r_B$. ∎

This is the ball-containment condition the balls-and-cones chapter used with hand-placed regions; the entire ELEm construction is that inequality with a hinge wrapped around it and a gradient pushed through it. Under the reading "$A \sqsubseteq B$ means ball $A$ inside ball $B$," the criterion turns a logical entailment into one scalar comparison, which is what makes both the training loss and the final probe possible.

The experiment end to end: Volume 2's axioms become 15 hinge losses (one role chain skipped out loud), gradient descent arranges 13 balls and 2 translations, and the soundness probe scores the trained geometry against the reasoner's 8 gold subsumptions. Original diagram by the authors, created with AI assistance.

Five hinges from four normal forms

Each trainable axiom contributes one penalty of the form $\max(0, g)$, a hinge: the quantity $g$ measures by how much the axiom's geometric constraint is violated, the hinge charges nothing when the constraint holds ($g \le 0$) and charges the violation itself when it does not. A hinge is not differentiable at its kink $g = 0$, so the code uses the standard subgradient convention: the gradient of $\max(0, g)$ is $\partial g / \partial \theta$ wherever $g \gt 0$ and the zero vector wherever $g \le 0$ (el_embed.py lines 140–142). One more standing fact, derived once and reused by every loss: the gradient of a norm. Writing $n(u) = \lVert u \rVert = \big(\sum_{j=1}^{d} u_j^2\big)^{1/2}$, the partial derivative in coordinate $j$ is, by the chain rule on the square root,

$$\frac{\partial n}{\partial u_j} \;=\; \tfrac{1}{2}\Big(\sum_k u_k^2\Big)^{-1/2} \cdot 2u_j \;=\; \frac{u_j}{\lVert u \rVert},$$

so $\partial \lVert u \rVert / \partial u = u / \lVert u \rVert$, the unit vector pointing along $u$, with subgradient $0$ chosen at the origin (el_embed.py lines 154–158). Here is the whole loss zoo at a glance, with $\gamma = 0$ the hinge margin and $\gamma_d = 0.1$ the disjointness margin (el_embed.py lines 45–46); the derivations follow.

form	axiom shape	geometric reading	hinge argument $g$	count
NF1	$A \sqsubseteq B$	ball $A$ inside ball $B$	$\lVert c_A - c_B \rVert + r_A - r_B - \gamma$	6
NF2	$A \sqcap B \sqsubseteq C$	balls overlap, midpoint region inside $C$	$\lVert c_A - c_B \rVert - (r_A + r_B) - \gamma$ and $\lVert m - c_C \rVert + \min(r_A, r_B) - r_C - \gamma$	1
NF3	$A \sqsubseteq \exists r.B$	ball $A$ shifted by $v_r$ inside ball $B$	$\lVert c_A + v_r - c_B \rVert + r_A - r_B - \gamma$	3
NF4	$\exists r.B \sqsubseteq A$	ball $B$ shifted back by $v_r$ meets ball $A$	$\lVert c_B - v_r - c_A \rVert - r_B - r_A - \gamma$	4
disjointness	$A \sqcap B \sqsubseteq \bot$	balls pushed at least $\gamma_d$ apart	$r_A + r_B - \lVert c_A - c_B \rVert + \gamma_d$	1

NF1: containment, hinged

The NF1 loss is the containment criterion of the previous section with the hinge wrapped around it:

$$L_{\mathrm{nf1}}(A, B) \;=\; \max\!\big(0,\; \lVert c_A - c_B \rVert + r_A - r_B - \gamma\big).$$

When the hinge is active, write $u = c_A - c_B$. The center gradients follow from the norm rule with $\partial u / \partial c_A = I$ (the identity: nudging $c_A$ nudges $u$ one-for-one) and $\partial u / \partial c_B = -I$: $\partial g / \partial c_A = u / \lVert u \rVert$ and $\partial g / \partial c_B = -u / \lVert u \rVert$. The radii enter linearly, $\partial g / \partial r_A = +1$ and $\partial g / \partial r_B = -1$, which the log-radius chain rule converts to $\partial g / \partial \rho_A = +r_A$ and $\partial g / \partial \rho_B = -r_B$. The code is the derivation transcribed (el_embed.py lines 160–172):

    # NF1  A ⊑ B : ball A inside ball B.
    #   L = max(0, ‖c_A − c_B‖ + r_A − r_B − γ)
    #   ∂L/∂c_A = u/‖u‖, ∂L/∂c_B = −u/‖u‖  (u = c_A − c_B);
    #   ∂L/∂r_A = +1, ∂L/∂r_B = −1  (so ∂L/∂ρ_A = +r_A, ∂L/∂ρ_B = −r_B).
    for a, b in NF1:
        n, u = unit(cent[a] - cent[b])
        g = n + rad[a] - rad[b] - GAMMA
        if g > 0.0:
            parts["nf1"] += g
            g_cent[a] += u
            g_cent[b] -= u
            g_rho[a] += rad[a]
            g_rho[b] -= rad[b]

Read the update's direction: a violated containment pulls $c_A$ toward $c_B$ (the step subtracts the gradient, so $c_A$ moves against $+u$, toward $c_B$), pushes $c_B$ toward $c_A$, shrinks $r_A$, and grows $r_B$. All four motions reduce the violation; gradient descent discovers set inclusion as a squeezing motion.

NF3 and NF4: the role translation, and why the side flips the sign

An existential restriction needs the role. ELEm reads "the $r$-successor of a point $x$" as the translated point $x + v_r$, so the axiom $A \sqsubseteq \exists r.B$ (every $A$ has an $r$-successor in $B$) becomes "ball $A$, shifted by $v_r$, sits inside ball $B$":

$$L_{\mathrm{nf3}}(A, r, B) \;=\; \max\!\big(0,\; \lVert c_A + v_r - c_B \rVert + r_A - r_B - \gamma\big),$$

a containment again, with $u = c_A + v_r - c_B$, gradients $\partial g/\partial c_A = \partial g/\partial v_r = u/\lVert u \rVert$ (the translation appears inside $u$ with coefficient $+1$, so it receives the same gradient as $c_A$), $\partial g/\partial c_B = -u/\lVert u \rVert$, and radius derivatives $+1, -1$ as in NF1 (el_embed.py lines 210–223).

NF4 puts the existential on the left: $\exists r.B \sqsubseteq A$ says anything with an $r$-edge into $B$ is an $A$. The region being constrained is now a pre-image, the set of points whose translate lands in ball $B$, which under the translation reading is ball $B$ shifted backward, centered at $c_B - v_r$. ELEm's hinge relaxes "that region lies inside $A$" to "that region is within reach of $A$," an overlap condition (el_embed.py lines 225–239):

$$L_{\mathrm{nf4}}(r, B, A) \;=\; \max\!\big(0,\; \lVert c_B - v_r - c_A \rVert - r_B - r_A - \gamma\big).$$

Here is the sign flip the table shows, decoded. In a containment (NF1, NF3), the inner radius and the outer radius fight: growing the inner ball makes containment harder ($+r_A$), growing the outer makes it easier ($-r_B$). In an overlap (NF4), both radii help: growing either ball makes the two easier to touch, so both enter with a minus sign, and the hinge only fires when the back-translated ball is separated from ball $A$ by more than the sum of the radii. The subgradients follow the same norm rule with $u = c_B - v_r - c_A$: $\partial g/\partial c_B = u/\lVert u \rVert$, $\partial g/\partial v_r = \partial g/\partial c_A = -u/\lVert u \rVert$, and $\partial g/\partial r_B = \partial g/\partial r_A = -1$, hence $-r_B$ and $-r_A$ after the log-radius conversion.

NF2: the awkward one

The conjunction axiom $A \sqcap B \sqsubseteq C$ asks the geometry for the region $A \sqcap B$, and the previous chapter proved that region is a lens, not a ball: the family is not closed under intersection, so no exact ball rendering exists and any NF2 loss is a surrogate. ELEm's surrogate, in the simplified midpoint form the companion module implements, imposes two hinges (el_embed.py lines 174–208): the operand balls must overlap,

$$g_1 \;=\; \lVert c_A - c_B \rVert - (r_A + r_B) - \gamma,$$

and the midpoint $m = \tfrac{1}{2}(c_A + c_B)$ of the two centers, carrying the smaller radius, must fit inside $C$:

$$g_2 \;=\; \lVert m - c_C \rVert + \min(r_A, r_B) - r_C - \gamma.$$

(The published loss constrains $\lVert c_A - c_C\rVert$ and $\lVert c_B - c_C\rVert$ with two separate hinges [1]; the midpoint form implements the same geometric intent with one, and it is what the code differentiates, as its comment states at lines 174–180.) The overlap hinge differentiates like NF4, radii negative: $\partial g_1/\partial c_A = u/\lVert u \rVert$, $\partial g_1/\partial c_B = -u/\lVert u \rVert$, $\partial g_1/\partial r_A = \partial g_1/\partial r_B = -1$. The midpoint hinge has two new wrinkles, both handled by the chain rule. Because $\partial m / \partial c_A = \tfrac{1}{2} I$, the gradient flowing into either operand center is halved: writing $w = m - c_C$, $\partial g_2/\partial c_A = \partial g_2/\partial c_B = w / (2\lVert w \rVert)$ while $\partial g_2/\partial c_C = -w/\lVert w \rVert$. And $\min(r_A, r_B)$ is itself kinked; its subgradient routes the $+1$ entirely to whichever radius is currently smaller, to $r_A$ on a tie (el_embed.py lines 199–208). Keep this loss in view: it is the one place the geometry is structurally unable to say what the logic says.

Disjointness: where balls are natural

The disjointness axiom Professor ⊓ Student ⊑ ⊥ is an NF2 whose right side is ⊥, and the compiler routes it to its own bucket (el_embed.py lines 103–108). ⊥ has no ball, so the axiom trains a single separation hinge, weighted by $w = 2$ (the DISJ_WEIGHT of line 51, standing in for the negative sampling the full recipe uses):

$$L_{\mathrm{disj}}(A, B) \;=\; w \cdot \max\!\big(0,\; r_A + r_B - \lVert c_A - c_B \rVert + \gamma_d\big).$$

The hinge fires while the balls overlap or come closer than the margin $\gamma_d = 0.1$; the distance now enters $g$ with a minus sign and both radii with a plus sign, so with $u = c_A - c_B$ the subgradients are $\partial g/\partial c_A = -u/\lVert u \rVert$, $\partial g/\partial c_B = +u/\lVert u \rVert$, $\partial g/\partial r_A = \partial g/\partial r_B = +1$, and the step drives the centers apart and shrinks both radii (el_embed.py lines 241–255). Notice the contrast with NF2: conjunction asked balls for a shape they cannot make, but disjointness asks only that two balls not touch, and "two balls not touching" is exactly one inequality. This is the constraint the ball family expresses natively, and the trained geometry will pass it with room to spare. A soft regularizer completes the loss, $\lambda \sum_A (\lVert c_A \rVert - 1)^2$ with weight $\lambda = 0.05$ (how strongly the pull toward the unit sphere counts against the axiom hinges), drawing every center toward the unit sphere as a differentiable stand-in for the hard normalization the original recipe applies; its gradient is $2\lambda(\lVert c_A \rVert - 1)\, c_A/\lVert c_A \rVert$ by the same norm rule (el_embed.py lines 257–263).

What zero loss would mean, and why we cannot have it

Every hinge charges exactly the violation of its geometric constraint, so "total loss equals zero" is a precise statement: all 15 constraints hold. How much logic that buys depends on the hinge, and here the five hinges split. For NF1 and NF3, the constraint is the axiom under the geometric reading (a containment, a shifted containment), so at zero loss those axioms would hold exactly. The disjointness hinge demands slightly more than its axiom: it vanishes only once the balls are separated by the extra margin $\gamma_d$, so it can stay positive on balls that are already disjoint, but its zero still forces the separation, hence the axiom. The other two hinges are strictly weaker than their axioms. The NF4 hinge relaxed "the back-shifted ball lies inside $A$" to a mere overlap, and the NF2 midpoint surrogate constrains one point and the smaller radius rather than the whole lens: a point $x$ in both operand balls satisfies only $\lVert x - m \rVert = \lVert \tfrac{1}{2}(x - c_A) + \tfrac{1}{2}(x - c_B) \rVert \le \tfrac{1}{2}(r_A + r_B)$, and $\tfrac{1}{2}(r_A + r_B)$ exceeds $\min(r_A, r_B)$ whenever the radii differ, so a zero-loss geometry can leave part of $A \sqcap B$ outside $C$. Zero loss therefore does not certify a model: the construction's own title promises a "geometric construction of models" [1], but its zero set contains geometries in which an NF4 or NF2 axiom is false. That gap between "loss zero" and "is a model" is the faithfulness critique the box-based successors open with [5], and closing it is the arc of the rest of Part III.

Even a genuine model, moreover, would buy trust in one direction only. An entailed subsumption holds in every model of the axioms, so a geometry that really modeled the trainable fragment could miss none of the entailments: perfect recall. But truth in one model is not entailment. A single model may nest two balls that no axiom relates, and that nesting asserts nothing about the logic; false positives can survive even at zero loss. This asymmetry is why the probe below must score precision, not just recall.

Our TBox forbids even the zero-loss starting point, and the proof is three lines of triangle inequality. Suppose the loss were zero. The two NF1 hinges of TenuredStudent would give exact containments, $\lVert c_{TS} - c_P \rVert + r_{TS} \le r_P$ and $\lVert c_{TS} - c_S \rVert + r_{TS} \le r_S$ (subscripts $TS$, $P$, $S$ for TenuredStudent, Professor, Student), and the disjointness hinge would give the separation $\lVert c_P - c_S \rVert \ge r_P + r_S + \gamma_d$. Chain the triangle inequality through $c_{TS}$ and substitute the two containments, each rearranged to bound a center distance:

$$\lVert c_P - c_S \rVert \;\le\; \lVert c_P - c_{TS} \rVert + \lVert c_{TS} - c_S \rVert \;\le\; (r_P - r_{TS}) + (r_S - r_{TS}) \;=\; r_P + r_S - 2 r_{TS}.$$

Combining with the separation, $r_P + r_S + \gamma_d \le r_P + r_S - 2 r_{TS}$, hence $2 r_{TS} \le -\gamma_d = -0.1$. But $r_{TS} = e^{\rho_{TS}}$ is positive by construction. Contradiction. The same algebra run without assuming zero loss yields a quantitative floor: the two TenuredStudent hinges plus the disjointness hinge must always sum to at least $\gamma_d + 2 r_{TS} \gt 0.1$, so the printed loss can never fall below that. The unsatisfiable concept is a stone in the optimizer's shoe, permanently.

This is why the chapter needs an instrument beyond the loss curve. Training will stop at some low, nonzero loss; every constraint then holds only approximately, so even the recall half of the guarantee frays, and the precision half never existed in the first place. What the trained geometry actually asserts, and how much of that the logic licenses, is an empirical question, and the honest way to answer it is to measure: freeze the geometry, define a geometric subsumption test, and score it against the reasoner. That is the soundness probe.

The committed training trace

Training is plain full-batch gradient descent on the summed loss, the update rule of Volume 1 applied simultaneously to all three parameter blocks (el_embed.py lines 288–295):

    for epoch in range(1, epochs + 1):
        loss, g_cent, g_rho, g_vrel, parts = loss_and_grads(cent, rho, vrel)
        if epoch in SNAPSHOTS:
            losses[epoch] = (loss, parts)
        # Gradient descent, θ ← θ − η ∂L/∂θ, on all three parameter blocks.
        cent -= LR * g_cent
        rho -= LR * g_rho
        vrel -= LR * g_vrel

Initialization is seeded (default_rng(0), line 281), centers on the unit sphere, every radius at $0.5$, translations small Gaussians, so reruns are byte-identical. With learning rate $\eta = 0.05$ for 3000 epochs, the committed run logs the loss, broken into its per-form pieces, at four snapshots (the loss before each snapshot epoch's update, so epoch 1 shows the untrained geometry):

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

Three things in this table deserve a slow read. First, the easy constraints die fast: the single NF2 axiom (Person ⊓ _N1 ⊑ Researcher, from normalizing axiom 14) and all four NF4 axioms are at 0.0000 by epoch 100 and stay there. Second, the total is not monotone: it falls to 0.6078 by epoch 1000 and rises to 0.6848 by epoch 3000, the disjointness piece climbing from 0.4168 to 0.4943. That is the frustrated triangle from the impossibility proof in motion: the TenuredStudent hinges pull Professor and Student together, the weighted disjointness hinge pushes them apart, and fixed-step gradient descent circulates around the unreachable optimum instead of settling, never able to drop below the floor the algebra predicted. Third, the printed radii of the trained balls recover the concept hierarchy by size:

the trained balls (named concepts, largest radius first)
  concept                 ‖c_A‖     r_A
  Person                 1.0000  1.1454
  Researcher             1.0000  0.9984
  Paper                  1.0000  0.5860
  Institution            1.0000  0.5000
  Topic                  1.0000  0.5000
  Student                1.0410  0.2615
  Professor              0.9980  0.1865
  TenuredStudent         0.9799  0.0270  (unsatisfiable)
  TenuredStudentAdvisor  0.9635  0.0069  (unsatisfiable)
  Dean                   1.0253  0.0059

Person is the biggest ball, Researcher next, then the siblings Student and Professor, then Dean, tiny and nested three containments deep; nobody told the model this ordering, it fell out of stacking containment constraints. Institution and Topic sit at radius exactly $0.5000$ with $\lVert c_A \rVert = 1.0000$: they occur in no TBox axiom, so no hinge ever touched them and their parameters are still the untrained initialization, incidental proof that every other number in the table was earned. And the two unsatisfiable concepts have been crushed toward radius zero; hold that thought for two sections.

The soundness probe

The instrument is one inequality. Define the geometric subsumption test as the containment criterion with a frozen slack $\varepsilon = 0.15$ (el_embed.py lines 301–305):

def sub_geo(a: str, b: str, cent: np.ndarray, rad: np.ndarray) -> bool:
    """The geometric subsumption test: does ball A sit inside ball B, up to
    the frozen slack ε?   sub_geo(A, B) := ‖c_A − c_B‖ + r_A ≤ r_B + ε."""
    ia, ib = C_ID[a], C_ID[b]
    return float(np.linalg.norm(cent[ia] - cent[ib])) + rad[ia] <= rad[ib] + EPS

The slack acknowledges that training stopped at nonzero loss: a containment holding up to a residual smaller than $\varepsilon$ still counts. The tolerance was tuned once for this suite and then frozen (line 55); an $\varepsilon$ adjusted after seeing the results would make the probe circular. The probe (el_embed.py lines 308–324) evaluates sub_geo on every ordered pair of satisfiable named concepts, $8 \cdot 7 = 56$ pairs, and scores each against Volume 2's gold set: asserted and entailed is a true positive (TP); asserted but not entailed, a false positive (FP); entailed but not asserted, a false negative (FN); neither, a true negative (TN). Precision is TP/(TP+FP), the fraction of the geometry's assertions that are logically sound; recall is TP/(TP+FN), the fraction of the logic's entailments the geometry recovers. The committed run:

soundness probe: sub_geo(A,B) := ‖c_A − c_B‖ + r_A ≤ r_B + ε, ε=0.15
  all 8·7 = 56 ordered pairs of satisfiable named concepts vs the 8 gold subsumptions
                     gold ⊑   not entailed
  geometry says ⊑    TP  8      FP  0
  geometry says no   FN  0      TN 48
  precision = 1.0000   recall = 1.0000
  false positives: none
  false negatives: none

	gold entails ⊑	gold does not
geometry asserts ⊑	TP = 8	FP = 0
geometry denies	FN = 0	TN = 48

On this TBox the trained balls recover the gold standard cleanly: all 8 entailed subsumptions asserted, none of the 48 non-entailments asserted. Say that honestly, and then dissect it, because both halves of the perfection have structural explanations that do not survive scale.

The perfect recall is partly geometry doing logic's work for free. Only 4 of the 8 gold pairs are asserted NF1 axioms between named concepts (Dean ⊑ Professor, Professor ⊑ Researcher, Student ⊑ Researcher, Researcher ⊑ Person); the other 4 are entailments the completion algorithm derived by transitivity. Exact ball containment is itself transitive, by the same triangle-inequality pattern as before: if $\lVert c_A - c_B \rVert + r_A \le r_B$ and $\lVert c_B - c_C \rVert + r_B \le r_C$, then

$$\lVert c_A - c_C \rVert + r_A \;\le\; \lVert c_A - c_B \rVert + \lVert c_B - c_C \rVert + r_A \;\le\; (r_B - r_A) + (r_C - r_B) + r_A \;=\; r_C .$$

So training only the asserted containments hands the geometry the derived ones automatically. One honest caveat: with slack, the argument degrades, since two containments each holding up to $\varepsilon$ compose to one holding up to $2\varepsilon$ while the probe grants only $\varepsilon$; the trained model happened to leave enough headroom that all four derived pairs passed anyway. The perfect precision, meanwhile, is what a 14-axiom TBox in $\mathbb{R}^8$ buys: with so few constraints and so much room, balls no axiom relates stay wherever random initialization scattered them, far apart in $\mathbb{R}^8$, and none of the 48 innocent pairs started or ended accidentally nested. The module's own competency check demands only TP ≥ 6 (el_embed.py lines 358–360) precisely because this cleanliness is a property of the run, not of the method; its docstring flags stray containments as the expected failure mode. At scale the picture inverts. ELEm itself was built for the Gene Ontology, and its own reported evaluation was protein-protein interaction link prediction rather than subsumption prediction [1]. The subsumption-prediction studies that came later, on GALEN, the Gene Ontology, and the anatomy ontology, are where ball embeddings are shown losing exactly where this chapter's analysis points, conjunction-heavy axiom sets whose NF2 surrogates cannot all be satisfied together, degrading recall of entailed subsumptions and letting unlicensed containments through [5][6]. The tiny TBox gives the method its best case; the probe methodology, not the 1.0000, is what transfers.

Disjointness, checked with a ruler

The one axiom the ball family expresses natively deserves its own verdict. The committed run measures the trained Professor and Student balls directly:

disjointness check: Professor ⊓ Student ⊑ ⊥, geometrically
  ‖c_Prof − c_Stud‖ = 0.5597  vs  r_Prof + r_Stud = 0.4480  →  gap +0.1117 (balls disjoint)

The centers sit $0.5597$ apart while the radii sum to only $0.4480 = 0.1865 + 0.2615$: the balls are disjoint with a gap of $+0.1117$, slightly more than the demanded margin $\gamma_d = 0.1$, and the module asserts the gap is positive (el_embed.py lines 361–364). No point of space is in both balls, so the geometric reading of "nobody is both a professor and a student" holds exactly in the trained model. Where conjunction was the family's structural weakness, disjointness is its structural strength: one inequality, natively expressible, verified with a ruler.

The two impossible concepts, or where the analogy frays

Volume 2's completion algorithm proved TenuredStudent ⊑ ⊥ and, through the bottom rule crawling backward along advises, TenuredStudentAdvisor ⊑ ⊥: in every genuine model of the TBox, both concepts denote the empty set. Now look at what the geometry did with them. It cannot make them empty. A ball of radius $e^{\rho} \gt 0$ always contains points, and the parameterization was chosen so radii cannot reach zero; there is no ball for ⊥, no geometric object that means "nothing." The optimizer's best compromise is visible in the radius table: TenuredStudent crushed to $r = 0.0270$, TenuredStudentAdvisor to $0.0069$, each a speck wedged between constraints that cannot all be met. The speck still asserts something false under the model-theoretic reading: it is a nonempty region, a claim that some possible individual is a tenured student, which the logic flatly refutes. The probe excludes unsatisfiable concepts from its 56 pairs (an unsatisfiable concept is vacuously subsumed by everything, so the comparison would be meaningless), and the honest statement is that ELEm has no rendering of unsatisfiability at all: it renders "impossible" as "very small," a category error rather than an approximation error. This is a second expressive gap, subtler than the skipped role chain but of the same kind, and it is one of the specific defects the box-based successors repair, since a box, unlike a ball, can be genuinely empty when a lower corner exceeds an upper corner.

The unsolved part

Tally the honest ledger. Of the 16 normal forms, one (the role chain) got no loss at all; one (the conjunction) got a loss that is a surrogate by mathematical necessity, because the previous chapter proved the true region is a lens no ball can be; one meaning (⊥, emptiness) has no geometric rendering, so unsatisfiability becomes smallness. On this TBox the damage stayed invisible: the single NF2 hinge hit zero by epoch 100 and the probe came back perfect. But the weakness is load-bearing at scale, where thousands of NF2 axioms interlock and the midpoint surrogate must trade violations off against containments it cannot coexist with. The open question is sharper than "do better on benchmarks." Is there any training objective over balls whose zero set exactly characterizes the models of an EL TBox with conjunctions, or is the closure failure a hard ceiling, so that every ball objective must either under-assert (losing entailments) or over-assert (inventing them)? The lens chapter's 60.56 percent area verdict says the ceiling is real and the fix must change the shape, not the loss. That is a falsifiable claim, and the next chapter tests it by rerunning this entire experiment, same TBox, same normalization, same gold, same probe, with boxes in place of balls, where intersection is exact corner arithmetic. The two confusion tables will sit side by side.

Why it matters

This chapter is the volume's first complete instance of the pattern the whole neuro-symbolic program depends on: take a symbolic artifact with exact semantics, compile it into a differentiable objective, train, and then audit the result against the symbolic ground truth rather than against a vibe. Reusing Volume 2's normalize() and classify() made the experiment controlled; the zero-loss analysis made "the geometry is a model" a precise claim rather than a metaphor, and showed exactly which hinges fall short of it; the impossibility proof said in advance that perfection was off the table, which is exactly what made a quantitative probe necessary; and the probe returned numbers a claim of "the embedding respects the ontology" can be held to. Volume 4 will build systems where the loss is the logic (semantic loss, differentiable proving), and Volume 5 will ask when a learned reasoner's outputs can be trusted; both inherit this chapter's discipline and its vocabulary. When someone says an embedding "captures" an ontology, the question this chapter installs permanently is: what is the probe, what is the gold standard, and what were the false positives?

Key terms

• EL++ TBox (terminological box) — the schema-level half of an ontology: the concept and role axioms, written in EL++, the lightweight description logic Volume 2 classified; here the same 14 academic-world axioms, normalized to 16 normal forms.
• ELEm (EL Embeddings) — the construction mapping each concept of an EL++ TBox to a ball in $\mathbb{R}^8$ and each role to a translation vector, trained so each normal-form axiom's geometric constraint holds; introduced as a geometric construction of models [1].
• Ball containment criterion — $B(c_A, r_A) \subseteq B(c_B, r_B)$ if and only if $\lVert c_A - c_B \rVert + r_A \le r_B$; derived from the triangle inequality in both directions, and the germ of every loss and of the probe.
• Hinge / subgradient — the penalty $\max(0, g)$ charging exactly the constraint violation; its gradient is $\partial g/\partial \theta$ where $g \gt 0$ and zero elsewhere, with the convention $\partial\lVert u \rVert/\partial u = u/\lVert u \rVert$.
• Log-radius $\rho_A$ — the parameterization $r_A = e^{\rho_A}$ keeping radii positive; converts radius gradients by $\partial L/\partial \rho_A = (\partial L/\partial r_A)\, r_A$.
• Role translation $v_r$ — the vector reading "$r$-successor of $x$" as $x + v_r$; routes NF3 as a shifted containment and NF4 as a back-shifted overlap.
• Geometric model / faithfulness — a geometry in which every trainable axiom is true under the geometric reading; ELEm's zero loss does not certify one (the NF4 and NF2 hinges are weaker than their axioms, the faithfulness gap the box methods target [5]), and even a model would guarantee only recall, since truth in one model is not entailment; zero loss is provably unreachable here anyway because of the unsatisfiable concepts.
• Soundness probe — the frozen test $\mathrm{sub\_geo}(A,B) := \lVert c_A - c_B \rVert + r_A \le r_B + \varepsilon$ scored against the reasoner's classification over all ordered pairs of satisfiable named concepts; here TP 8, FP 0, FN 0 over 56 pairs.
• Expressive gap — a meaning the construction leaves unrendered: the role chain $r \circ r \sqsubseteq s$ receives no loss term (skipped, out loud), and unsatisfiability has no geometric rendering at all (no ⊥ ball; "impossible" rendered as "very small").

Where this leads

The conjunction was the confessed weak point, and the previous chapter proved the weakness is the shape's, not the optimizer's. The next chapter, BoxEL and Box²EL, swaps the shape: concepts become axis-aligned boxes, whose intersections are boxes computed exactly by corner arithmetic, so the NF2 constraint can finally say what the axiom says; a box can also be genuinely empty, giving ⊥ a real denotation. The experiment reruns unchanged — the same 14 axioms through the same normalize(), the same gold classification, the same 56-pair probe — and the resulting confusion table goes next to this one. The question it answers is the one this chapter earned the right to ask: how much soundness does a shape buy?

---

Companion code: examples/neural/el_embed.py implements this entire chapter: the reuse of Volume 2's normalization and classification (lines 37–40 and 59–126), all five hinge losses with their hand-derived subgradients in comments directly above the code (lines 129–266), full-batch training (lines 271–296), the geometric subsumption test and probe (lines 299–324), and the competency asserts guarding every claim made here (lines 346–364). Run python3 examples/neural/el_embed.py to reproduce every number in this chapter byte for byte; the run ends with 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.