The Honest Verdict: What Vectors Can and Cannot Hold

📍 Where we are: Part VI · The Verdict — Chapter 18. Soft Unification ended Part V with a proof that goes through on a kernel score rather than a certificate; now we close the volume by totalling the ledger that score belongs to: what vectors genuinely hold, and what only symbols guarantee.

This chapter adds no new model. It audits the whole volume, deliberately in the mirror-image structure of Volume 2's closing verdict: a column of things the geometry genuinely delivers, a column of things it cannot, and a runnable ledger behind every row. Across seventeen chapters you embedded the academic knowledge graph as points, translations, bilinear forms, balls, boxes, Beta densities, hyperbolic coordinates, message-passing states, attention maps, holographic vectors, and soft proofs. Every load-bearing number was committed output of a seeded module, so the verdict does not rest on rhetoric. It rests on validate.py, whose exit code is the volume's acceptance verdict, and on an independent oracle, torch_check.py, which recomputed the three load-bearing loss gradients under torch.autograd and agreed to machine precision; the suite's remaining hand-derived calculus is guarded module by module, two of them with their own central-difference checks, and the methodology section below states exactly which check covers what.

The simple version

Imagine the meticulous auditor of Volume 2 sharing an office with a veteran talent scout. The auditor certifies only what the receipts prove and refuses to guess; the scout has watched ten thousand games and will tell you, with unnerving accuracy, which unknown player is probably great, unbothered by a misspelled name or a missing match report. But the scout can certify nothing: you get odds, never receipts, and when pressed for a proof the scout shrugs and points at a feeling trained into years of watching. This volume hired the scout. The verdict is the moment we write both job descriptions on one page and admit that neither can do the other's work.

What this chapter covers

• The verdict, stated plainly: geometry buys you plausibility you can train, on knowledge you never wrote down, at the price of certainty you can no longer have.
• What is genuinely solid: the MRR (mean reciprocal rank) lift over the frozen-random baseline, regions that carry logic exactly when constructed and recover it when trained, exact box conjunction, hierarchy at embedding dimension $d = 2$ in hyperbolic space, and a proof that survives a synonym, each with its committed number.
• What stays out of reach: no entailment guarantee at nonzero loss, DistMult's algebraically forced tie, the ball's unavoidable false-positive lens cover, the 1-WL (1-dimensional Weisfeiler-Leman) ceiling, capacity decay, and uncalibrated scores.
• The methodology as a result: every gradient in the suite is derived by hand; the three load-bearing loss families are certified against torch.autograd, two modules add their own central-difference checks, and the rest are vouched for by competency outcomes — the checking ledger stated exactly, and why an independent oracle matters.
• The evidence, made runnable: the 15/15 competency ledger, one check per claim, mapped to the chapter each check guards.
• The five recurring tensions: exact vs robust, proof vs score, discrete vs differentiable, constructed vs learned, and closure vs capacity, the axes Volume 4 must reconcile.
• Honest advice: keep the symbolic gold standard runnable next to every neural experiment; that discipline is neuro-symbolic method in miniature.

The verdict, stated plainly

Here is the whole finding in one line: geometry buys you plausibility you can train, on knowledge you never wrote down, at the price of certainty you can no longer have [1]. It is the exact mirror of Volume 2's verdict, that symbols buy correctness you can trust and explain on knowledge you must write down and keep consistent, and both clauses again carry weight. Plausibility you can train is the reward: TransE was never told that erin is affiliated with cmu, yet after gradient descent on the other committed triples it ranks the truth near the top, because the loss carved a geometry in which unwritten facts sit close to written ones. Certainty you can no longer have is the price: no score this volume produced is a theorem. A distance is not an entailment; it is a graded bet whose reliability we could only measure empirically, by holding the geometry up against Volume 2's exact classifier and counting where they disagree. The verdict is not a winner. It is a division of labor, and every row of it below is a number you can regenerate with one command.

The end-of-volume ledger: five green rows of things vectors genuinely hold, six rose rows of things only symbols guarantee, five tension sliders beneath, two runnable stamps in the footer, and a dashed arrow handing both columns to the integration volume. Original diagram by the authors, created with AI assistance.

What is genuinely solid

Five results in this volume are mechanical, reproducible, and guarded by named checks that either pass or turn the build red. Here is the ledger, then the elaboration.

what vectors hold	committed evidence	module	chapter
link prediction lifts ranking far above chance	filtered MRR $0.7778$ vs frozen-random baseline $0.1062$	transe.py	Translational Models
regions can carry logical structure exactly when constructed	$8/8$ gold subsumptions, $0$ spurious, $13/13$ memberships	regions.py	Balls and Cones
trained regions recover the classification	balls recover $8/8$ gold with $0$ spurious and $0$ missed; boxes the same, with exact conjunction (⊓, concept intersection)	el_embed.py, box_el.py	EL Embeddings, BoxEL and Box²EL
boxes make conjunction exact	$0$ mismatches on the dense membership grid	boxes_vs_balls.py	Boxes versus Balls
hyperbolic space fits hierarchy at $d = 2$	Spearman $0.8136$ vs Euclidean $0.7539$, same dimension	hyperbolic.py	Hyperbolic Embeddings
soft matching survives synonyms that kill the hard prover	soft proof scored $0.9783$ where hard unification returns nothing	soft_unification.py	Soft Unification

Plausibility over unwritten facts. The headline metric of Part I is the filtered mean reciprocal rank (MRR). Decode it before the symbols: for each of the $|Q| = 6$ ranking queries built from the 3 held-out test triples (one head query and one tail query each), the model sorts all 13 entities by score, other known-true answers are filtered out, and $\mathrm{rank}_i$ is the position of the gold entity in query $i$. Then

$$\mathrm{MRR} \;=\; \frac{1}{|Q|} \sum_{i=1}^{|Q|} \frac{1}{\mathrm{rank}_i},$$

so a perfect model scores $1.0$. Two reference points calibrate the scale. The committed frozen-random control, the seed-1 untrained geometry of Link Prediction run through the identical evaluation, scores $0.1062$; and the analytic chance line derived in that chapter is $0.2543$, because on a filtered pool of $m$ candidates every rank is equally likely, so the expected reciprocal rank is $\frac{1}{m}\sum_{k=1}^{m}\frac{1}{k}$, and averaging that quantity over the six queries' pools gives $0.2543$ (the frozen draw sits below its own expectation because it is one sample of a random geometry, not an average over draws). The committed run of transe.py lands at $\mathrm{MRR} = 0.7778$, with Hits@1, the fraction of queries whose gold answer is ranked first, at $0.6667$, the training loss falling from $1.5827$ to $0.0072$. A seven-fold lift over the frozen-random control, three-fold over the analytic chance level, on facts the model never saw: that is the neural pillar's core deliverable, and it is exactly what a symbolic reasoner, which abstains on anything unstated, cannot offer [1].

Regions can hold logic, exactly and then approximately. Part II showed by construction that the geometry is expressive enough: regions.py places balls by hand so that the geometric subsumption test reproduces all 8 of Volume 2's gold subsumptions with 0 spurious extras, all 7 disjointness pairs, and all 13 entity memberships. Part III then asked whether training can earn what construction proved. The probe design is the same in both ontology modules, but each region family carries its own containment test and tolerance. The ball probe asserts $A \sqsubseteq B$ (read "every $A$ is a $B$") exactly when ball $A$ sits inside ball $B$ with slack $\varepsilon$,

$$\lVert \mathbf{c}_A - \mathbf{c}_B \rVert + r_A \;\le\; r_B + \varepsilon,$$

where $\mathbf{c}_A$ is the ball's center, $r_A$ its radius, $\lVert \mathbf{c}_A - \mathbf{c}_B \rVert$ the Euclidean distance between the two centers (the straight-line length of their difference vector), and $\varepsilon = 0.15$ a tolerance fixed once and then frozen (el_embed.py line 55). The box probe measures instead, axis by axis, how far box $A$'s corners protrude outside box $B$, and accepts $A \sqsubseteq B$ when that worst-axis gap is at most its own tolerance $\varepsilon = 0.05$, three times tighter (box_el.py line 128). Scored over all $8 \cdot 7 = 56$ ordered pairs of satisfiable named concepts against the gold standard, the trained ELEm (EL Embeddings) balls produce a clean confusion table: 8 true positives, 0 false positives, 0 false negatives, 48 true negatives, precision and recall both $1.0000$. The trained BoxEL-style boxes match it, $8/8$, with the Professor and Student boxes kept genuinely apart (minimum per-axis overlap $-0.0304$, negative meaning separated on at least one axis).

Conjunction is exact when the family is closed. For boxes with lower corner $\mathbf{l}$ and upper corner $\mathbf{u}$, the intersection is again a box, computed coordinate-wise as $l_i^{\cap} = \max(l_i^A, l_i^B)$ and $u_i^{\cap} = \min(u_i^A, u_i^B)$, so membership in the intersection equals the conjunction of memberships, point for point. boxes_vs_balls.py verifies this identity on a dense grid and finds zero mismatches; the same module shows balls failing the same test, which we return to below.

Hierarchy fits in two curved dimensions. On the 22-node hierarchy, the Poincaré-ball embedding at $d = 2$ tracks the graph's own distances with Spearman rank correlation $0.8136$ (Spearman correlates the orderings of two distance lists, with $1.0$ meaning identical order), beating the Euclidean control at the same dimension, $0.7539$, with embedding norms increasing monotonically with depth. Exponentially growing trees are what negatively curved space is for, and the head-to-head makes the claim at equal parameter budgets.

Robustness to vocabulary drift. The hard prover of Volume 1 fails the query supervises(bob, Z) outright, because no fact uses the predicate supervises: hard unification requires symbol identity, and the knowledge base says advises. The soft prover of the previous chapter matches predicates by embedding similarity and completes the proof at score $0.9783$ through the kernel value $k(\text{supervises}, \text{advises}) = 0.9783$, returning the same two answers the hard prover finds for the original predicate, while the unrelated control query cites(bob, Z) stays safely below the acceptance threshold ($0.4621$ against $\tau = 0.80$). Synonyms are noise to a symbol table and signal to a geometry.

What stays out of reach

Now the other column. Each gap below is not an engineering shortfall awaiting a better learning rate; each is either an algebraic fact or the absence of a theorem, and each has its committed or cited evidence.

No model, no entailment guarantee. In logic, the guarantee flows from having a model: if the trained geometry satisfied every axiom exactly, it would be a model of the ontology, and every statement the ontology entails would then hold in the geometry, perfect recall on entailments (though one model among many can still satisfy extra containments the ontology never entails, so precision is not part of the promise). Zero loss would certify exactly that. The committed ELEm run bottoms out at loss $0.6848$, and it provably cannot reach zero: no geometry can place TenuredStudent inside both Professor and Student while the disjointness hinge holds those two balls apart by $\gamma_d$, the disjointness margin the hinge enforces (el_embed.py line 46 sets $\gamma_d = 0.1$), so the unsatisfiable concepts keep an irreducible residual. The clean $8/8$ confusion table above must therefore be read correctly: it is a measured outcome on a 14-axiom TBox (terminological axiom box, the ontology's set of concept-level axioms) with a tuned, frozen $\varepsilon$, not a consequence of any theorem. The probe is built for the day the table is not clean; el_embed.py lines 433-440 print every false positive by name, with the violated inequality spelled out and the verdict "unsound!" attached, because a trained ball can drift inside another with no axiom licensing it and nothing in the loss forbids that. The module's own docstring (lines 21-30) states the honest position: the trained model is not a sound reasoner, only an approximation of one, and the false positives, whenever they occur, are the story. One axiom never even reached the loss: the role chain advises ∘ advises ⊑ grandAdvisor (the composition symbol ∘ chains advises with itself: the advisor's advisor) has no ELEm expression at all, so 15 of the 16 normal forms were trained and the 16th was skipped out loud. BoxEL's lower residual ($0.0678$) shrinks the gap; it does not change its kind.

A model family can be wrong by algebra, before any training. DistMult scores a triple as $s(h, r, t) = \sum_{i=1}^{d} w_r[i]\, e_h[i]\, e_t[i]$, where $e_h, e_t$ are the head and tail entity vectors, $w_r$ the relation vector, and $i$ runs over the $d$ coordinates. Because each term is a product of three scalars and scalar multiplication commutes, $e_h[i]\, e_t[i] = e_t[i]\, e_h[i]$ in every coordinate, so $s(h, r, t) = s(t, r, h)$ for every parameter setting. No gradient step can ever break the tie. The committed run makes this concrete on the graph's antisymmetric citation relation: only the forward citation $(p2, \textit{cites}, p1)$ was ever trained as true, and yet:

  score                        DistMult    ComplEx
  s(p2, cites, p1)   true       4.8879     6.6413
  s(p1, cites, p2)   false      4.8879    -4.5805
  |forward - reverse|          0.0000     11.2217

DistMult scores the false reverse exactly as plausible as the true fact, to the last digit, while ComplEx's conjugated tail slot breaks the symmetry and separates the directions by $11.2217$. The ceiling shows up downstream too: DistMult's MRR is $0.1962$ against ComplEx's $0.5167$ on the same protocol. The lesson generalizes: expressiveness failures of a score function are theorems about the family, not defects of a run.

Balls cannot intersect exactly. The intersection of two balls is a lens, and a lens is not a ball, so a ball-based model must cover every conjunction with a ball that contains it. boxes_vs_balls.py computes the smallest enclosing ball of the lens where two radius-1.5 balls overlap and measures the cost on a deterministic dense grid: the lens has area $1.5487$, the best covering ball area $3.9270$, so $60.56\%$ of the cover is false-positive area, points asserted into the conjunction that belong to neither operand's overlap, with a concrete witness printed at $(-0.1173, -0.0160)$. This is geometry, not underfitting; it is the precise reason the box family, closed under intersection, earned its zero-mismatch row above.

Structure beyond 1-WL is invisible. Two disjoint triangles and one hexagon are provably non-isomorphic (one contains two triangles, the other none), yet the 1-dimensional Weisfeiler-Leman color refinement stabilizes after one round on their disjoint union with identical color histograms, six nodes of the single color on each side, printed by wl.py as identical = True. Since message-passing graph neural networks distinguish at most what 1-WL distinguishes, no such network, whatever its width, depth, or training budget, can embed 2×C₃ and C₆ differently [2]. The ceiling is logical, not statistical: the volume's expressiveness chapter located it exactly at the two-variable counting logic C².

One-vector memories decay with load. The holographic memory of Part V stores the entire 18-triple graph in a single 1024-dimensional vector and answers all 18 queries correctly. But superposition spends capacity: on the committed sweep over a 50-entity vocabulary, accuracy at $d = 64$ with 18 stored triples is already down to $0.2778$, and even at $d = 1024$ it slides from $1.0000$ at 18 triples to $0.6200$ at 200. The decay is graceful, which is the family's virtue, and it is decay nonetheless: a fixed-dimensional vector is a finite-bandwidth channel, not a database.

Scores are not calibrated probabilities. The Beta-embedding chapter answered the negated query affiliated with cmu and not advised by bob with the composed score $f_A \cdot (1 - f_B)$, where $f = e^{-\mathrm{KL}}$ turns a KL (Kullback-Leibler) divergence, the standard measure of how far one probability density sits from another, into a similarity in $(0, 1]$, ranking the gold answer erin first at $0.5864$ with dave a close second at $0.5266$. Restate that chapter's honest paragraph here, because it applies to every score in this volume: the ordering is meaningful and the values are not probabilities. Nothing in any training objective used here ties $0.5864$ to "right about 59 percent of the time"; these are learned compatibilities, monotone evidence at best, and treating them as posteriors is a category error that Volume 5 confronts under the name calibration.

The methodology as a result

One result of this volume is not about any model: it is about how the volume knows its own mathematics is right. Every gradient in the companion suite is derived by hand, no autograd anywhere in the training loops, with the formula in a comment above the code that applies it. Take the volume's first and most-used derivation, the TransE margin loss. With the residual $\mathbf{v} = \mathbf{e}_h + \mathbf{w}_r - \mathbf{e}_t$ and the distance $d = \lVert \mathbf{v} \rVert_2 = \big(\sum_{j} v_j^2\big)^{1/2}$ (the index $j$ running over the 16 embedding coordinates), the partial derivative of the distance with respect to one coordinate $v_i$ comes from the chain rule on the square root, every step shown:

$$\frac{\partial d}{\partial v_i} = \frac{1}{2}\Big(\sum_{j} v_j^2\Big)^{-1/2} \cdot 2 v_i = \frac{v_i}{d}, \qquad\text{so}\qquad \nabla_{\mathbf{v}}\, d = \frac{\mathbf{v}}{d},$$

a unit vector (here $\nabla_{\mathbf{v}}\, d$, with $\nabla$ read "nabla", is the gradient of $d$ with respect to the residual $\mathbf{v}$: the vector collecting all sixteen partial derivatives $\partial d/\partial v_i$ into one object). The loss $L = \max(0,\ \gamma + d_{\text{pos}} - d_{\text{neg}})$, where $\gamma$ is the fixed margin hyperparameter by which the positive distance must undercut the negative distance, has on its active branch $\partial L / \partial d_{\text{pos}} = +1$ and $\partial L / \partial d_{\text{neg}} = -1$; the residual depends on its three embedding rows through $\partial \mathbf{v}/\partial \mathbf{e}_h = I$, $\partial \mathbf{v}/\partial \mathbf{w}_r = I$, and $\partial \mathbf{v}/\partial \mathbf{e}_t = -I$ (identity and negated-identity Jacobians, $I$ the identity matrix), so the six per-row gradients are $\pm \mathbf{v}_{\text{pos}}/d_{\text{pos}}$ and $\mp \mathbf{v}_{\text{neg}}/d_{\text{neg}}$, each of norm exactly $1$. That is precisely the code at transe.py lines 92-108:

    # ∂‖v‖/∂v = v/‖v‖  (unit residual; subgradient 0 when ‖v‖ = 0).
    u_pos = v_pos / d_pos if d_pos > 0.0 else zero.copy()
    u_neg = v_neg / d_neg if d_neg > 0.0 else zero.copy()

    # Chain rule through the active hinge (∂L/∂d_pos = +1, ∂L/∂d_neg = -1),
    # with ∂v/∂e_h = I, ∂v/∂e_r = I, ∂v/∂e_t = -I:
    #   ∂L/∂e_{h_pos} = +v_pos/‖v_pos‖    ∂L/∂e_{h_neg} = -v_neg/‖v_neg‖
    #   ∂L/∂e_{r_pos} = +v_pos/‖v_pos‖    ∂L/∂e_{r_neg} = -v_neg/‖v_neg‖
    #   ∂L/∂e_{t_pos} = -v_pos/‖v_pos‖    ∂L/∂e_{t_neg} = +v_neg/‖v_neg‖
    grads = {
        "h_pos": u_pos.copy(),
        "r_pos": u_pos.copy(),
        "t_pos": -u_pos,
        "h_neg": -u_neg,
        "r_neg": -u_neg.copy(),
        "t_neg": u_neg.copy(),
    }

How does the suite know these hand-written formulas are correct? Not by one uniform mechanism, and stating the checking ledger exactly is part of the volume's honesty. Two modules verify their own calculus numerically, inside their own runs: bilinear.py compares every hand-derived DistMult and ComplEx partial, at both labels $y = \pm 1$, against central differences before training starts (the checker at lines 157-208, gated by the asserts at lines 303-304), and attention_demo.py does the same for the softmax Jacobian (jacobian_check, lines 144-159, gated by the assert at line 256). The suite's other manual gradients, including the TransE gradient just derived, the box corner gradients, the Beta KL gradients, the Riemannian updates, and the message-passing backpropagation, carry no in-module gradient check; they are vouched for indirectly, by the competency outcomes their training runs must reach, and indirect evidence is weaker, because a subtly wrong gradient could in principle still stumble to a passing score. That gap is one reason an oracle exists at all.

Even where a central-difference check does run, it leaves one rival hypothesis standing: the formula and its checker were written by the same hand, against the same reading of the loss (torch_check.py lines 6-13). Volume 2 faced the same rival for its from-scratch classifier and removed it with HermiT, an independent industrial reasoner that had to agree on every subsumption. This volume does the same for calculus instead of classification, on the three loss families the volume leans on hardest: the TransE margin hinge, the DistMult logistic loss, and the box inclusion hinge; for the TransE hinge and the box hinge, the oracle is the only independent check their gradients receive. torch_check.py rebuilds each of the three losses from float64 leaf tensors copied from the same seeded arrays the manual code sees, lets torch.autograd differentiate with no sight of the manual gradients, and demands agreement below $10^{-6}$ per gradient row. The torch side of the TransE check is six lines (torch_check.py lines 131-136):

    d_pos = torch.linalg.vector_norm(
        leaves["h_pos"] + leaves["r_pos"] - leaves["t_pos"])
    d_neg = torch.linalg.vector_norm(
        leaves["h_neg"] + leaves["r_neg"] - leaves["t_neg"])
    loss_t = torch.relu(transe.GAMMA + d_pos - d_neg)
    loss_t.backward()

The protocol is careful where calculus is genuinely ambiguous: the checked TransE pair is chosen deterministically so the hinge is active and clear of its kink (pre-hinge margin $3.9333$), because at the kink a manual subgradient and autograd's relu rule may legitimately pick different values, and an inactive hinge would make the whole comparison vacuous, all zeros against all zeros (torch_check.py lines 86-106). The same discipline covers DistMult's logistic loss $L = \mathrm{softplus}(-y s)$ at both labels $y = +1$ and $y = -1$, where $\mathrm{softplus}(x) = \ln(1 + e^x)$ is the smooth hinge, and the squared box-inclusion hinge with its four corner gradients $\partial L/\partial \mathbf{l}_A = -2\,\mathbf{h}_{\text{lo}}$ and companions, where $\mathbf{h}_{\text{lo}} = \max(0,\ \mathbf{l}_B - \mathbf{l}_A + \gamma)$ collects, coordinate by coordinate, how far box $A$'s lower corner violates inclusion in box $B$ under the box module's own margin $\gamma$ (zero wherever the inclusion holds), on corner draws re-seeded until every pre-hinge term clears the kink by at least $10^{-3}$ (lines 225-256). The closing lines of the committed run (in the full transcript each PASS line ends its check's multi-line per-slot diff table; those tables are elided here as ...):

   ...
   PASS transe (max |Δ| = 5.6e-17)
   ...
   PASS distmult (max |Δ| = 2.8e-17)
   ...
   PASS box_incl (max |Δ| = 0.0e+00)

AGREEMENT CONFIRMED: manual gradients match torch.autograd
SUMMARY torch_check: transe=5.6e-17 distmult=2.8e-17 box=0.0e+00 checks=3/3 tol=1e-06

Agreement at the level of $10^{-17}$ is pure floating-point rounding: two independent implementations computed the same mathematics. The certificate's scope is exactly the three families every headline ranking number flows through; the rest of the suite's calculus stands on the two in-module central-difference checks and on the competency ledger of the next section, and the chapter has now said which is which. Treat this as a result of the volume in its own right, because the empirical literature says the surrounding hygiene is not optional decoration: on the standard benchmarks, retuning training protocols moves knowledge-graph-embedding results as much as changing the model does [3]. A number without its seed, its protocol, and an independent check is an anecdote.

The evidence, made runnable

Every claim above is one row of validate.py, the Volume 3 acceptance harness. Each named check calls a companion module's run(), which retrains (or reconstructs) its model deterministically and executes its own competency asserts; the harness prints one PASS or FAIL line per claim and exits 0 only if every check holds (validate.py lines 71-86):

    for claim, check in _checks():
        try:
            if verbose:
                check()
            else:
                with contextlib.redirect_stdout(io.StringIO()):
                    check()
            print(f"PASS  {claim}")
            passed += 1
        except AssertionError as exc:
            print(f"FAIL  {claim}  ({exc})")
            failed += 1
    total = passed + failed
    print(f"\nneural companion: {passed}/{total} competency checks passed"
          f"  ({time.time() - t0:.0f}s)")
    return 0 if failed == 0 else 1

Running it prints the volume's real bottom line:

PASS  TransE lifts filtered MRR far above the frozen-random baseline
PASS  DistMult's two cites directions tie exactly; ComplEx breaks the tie
PASS  constructed balls reproduce all 8 gold subsumptions with 0 spurious
PASS  Query2Box boxes answer multi-hop queries that match symbolic traversal
PASS  Beta negation is an exact involution and answers the negated query
PASS  the best ball around a lens admits false positives; box intersection is exact
PASS  trained ELEm balls recover the gold classification (soundness probe)
PASS  trained boxes match the probe with exact conjunction available
PASS  hyperbolic beats Euclidean at equal dimension on the hierarchy
PASS  the GCN is permutation-equivariant and 2-hop local to machine precision
PASS  typed weights beat untyped message passing; bases cut parameters
PASS  1-WL cannot separate two triangles from a hexagon; sum out-separates mean/max
PASS  attention rows are distributions; the Jacobian matches finite differences
PASS  one 1024-d vector stores the whole KG; capacity degrades gracefully
PASS  soft unification proves through a synonym where hard unification fails

neural companion: 15/15 competency checks passed  (16s)

Fifteen checks, one per central claim, each guarding the chapter that quotes its numbers (validate.py lines 30-64):

#	competency check	module	chapter it guards
1	TransE lifts filtered MRR far above the frozen-random baseline	transe.py	Link Prediction, Translational Models
2	DistMult's two cites directions tie exactly; ComplEx breaks the tie	bilinear.py	Bilinear Models
3	constructed balls reproduce all 8 gold subsumptions with 0 spurious	regions.py	Balls and Cones
4	Query2Box boxes answer multi-hop queries that match symbolic traversal	boxes.py	Box Embeddings
5	Beta negation is an exact involution and answers the negated query	beta.py	Beta and Probabilistic Embeddings
6	the best ball around a lens admits false positives; box intersection is exact	boxes_vs_balls.py	Boxes versus Balls
7	trained ELEm balls recover the gold classification (soundness probe)	el_embed.py	EL Embeddings
8	trained boxes match the probe with exact conjunction available	box_el.py	BoxEL and Box²EL, TransBox and mOWL
9	hyperbolic beats Euclidean at equal dimension on the hierarchy	hyperbolic.py	Hyperbolic Embeddings
10	the GCN is permutation-equivariant and 2-hop local to machine precision	gnn.py	Message Passing
11	typed weights beat untyped message passing; bases cut parameters	rgcn.py	Relational GNNs
12	1-WL cannot separate two triangles from a hexagon; sum out-separates mean/max	wl.py	The Expressiveness Ceiling
13	attention rows are distributions; the Jacobian matches finite differences	attention_demo.py	Attention
14	one 1024-d vector stores the whole KG; capacity degrades gracefully	vsa.py	Vector Symbolic Architectures
15	soft unification proves through a synonym where hard unification fails	soft_unification.py	Soft Unification

Every claim in this volume has a command the reader can run: python3 validate.py for the ledger, python3 <module>.py for any single chapter's trace, and the optional python3 torch_check.py for the oracle. The day a claim stops being true, main returns 1 and the build turns red.

The five recurring tensions

The gaps are not six unrelated complaints. They organize into five axes, each anchored in a chapter of this volume, and together they are the requirements document Volume 4 inherits.

Exact vs robust. Volume 2's classifier is exactly right or exactly silent; delete one fact and it abstains without complaint. This volume's models answer everything, usefully but approximately: the $0.7778$ MRR earned under the protocol of Link Prediction is a triumph because the questions were unanswerable exactly. Neither pole can impersonate the other, and no chapter here dissolved the axis; each just chose a point on it.

Proof vs score. A hard proof is a certificate: every step is an axiom or a rule application, checkable forever. The soft proof of Soft Unification that scored $0.9783$ is a similarity-weighted chain whose acceptance hinges on a threshold $\tau$; lower $\tau$ past $0.6806$, the vocabulary's worst random collision, and a spurious answer leaks in (the control query's own noise tops out lower, at $0.4621$). The score carries evidence but not validity, and nothing in this volume converts one into the other.

Discrete vs differentiable. Gradient descent needs slopes; symbols come in steps. Attention is the volume's cleanest exhibit: softmax is a differentiable stand-in for the discrete argmax lookup, exact only in the limit of orthogonal keys and sharp logits, and the $\sqrt{d_k}$ scaling ($d_k$ the dimension of the key vectors) exists precisely to keep the relaxation from saturating back into a step (maximum attention weight $0.9903$ unscaled versus $0.2282$ scaled). Even the oracle had to respect this axis, stepping deliberately around hinge kinks where the derivative stops being single-valued.

Constructed vs learned. Balls and Cones placed regions by hand and achieved perfect logical fidelity, proving the geometry expressive enough; EL Embeddings trained them and had to settle for a probe, a tuned $\varepsilon$, and a residual loss of $0.6848$. Construction proves possibility; learning delivers scale and generalization; the guarantee lives with the constructor, and this volume found no way to hand it to the learner.

Closure vs capacity. Demanding that a region family be closed under an operator buys exactness for that operator: boxes under intersection (Boxes versus Balls), Beta densities under negation. But every closure demand constrains the geometry, and pushing all structure into one representation spends a different budget: the holographic vector of Vector Symbolic Architectures is closed under binding and superposition and pays with recall falling from $1.0000$ to $0.6200$ as the load grows. Exactness of operators and capacity of the carrier trade against each other everywhere in this volume.

Honest advice for building neuro-symbolic systems

Volume 2 closed with the advice to model the crisp symbolic version of a task first. This volume can now state the companion habit it practiced throughout: keep the symbolic gold standard runnable next to every neural experiment. Not documented, not remembered: runnable. Our soundness probes only meant something because el_embed.py and box_el.py import Volume 2's normalize() and classify() and recompute the 8 gold subsumptions and 2 unsatisfiable concepts on every run, never retyping them, so the geometry was always graded against live logic rather than a stale transcript of it. Every strong claim in this volume has that shape: a neural artifact, a symbolic definition of truth, and an executable comparison between them. That discipline is neuro-symbolic method in miniature. It costs almost nothing on the day you adopt it, and everything on the day you need it and do not have it.

The unsolved part

Everything in this volume kept the two pillars side by side: train the geometry, then probe it against the logic, from the outside, after the fact. The honest open question is whether the comparison can move inside the loop without losing what makes each pillar worth having. If the logic becomes part of the loss, gradients can push the geometry toward the axioms, but a loss term is a preference, not a constraint: at any nonzero residual the guarantee is still absent, merely nearer. If instead the logic stays a hard filter, it is exact but gradient-opaque, and learning cannot feel it. Whether there exists machinery that is differentiable end to end and inherits a real soundness statement at the end of training, rather than an empirical confusion table, is not settled by anything this volume measured. The division of labor is established; whether it can become a genuine composition, with both signatures on one result, is exactly the question the next volume exists to attack [4].

Why it matters

This chapter is the second half of a two-column argument the series has been assembling since Volume 2's verdict. Symbols: correctness you can audit, on knowledge you must author. Vectors: plausibility you can train, without certainty. Neither column subsumes the other, and the committed evidence now shows both facts on one shared world, down to the digit. That is precisely the situation in which integration is not a slogan but a forced move [4]: a system that must both learn from data and guarantee its conclusions has to draw from both columns, and the five tensions above are the design constraints any such system must negotiate. The reader who carries this ledger forward can evaluate every Volume 4 method by asking one sharp question: which rows of the two columns does it actually merge, and at what price on which axis?

Key terms

• The verdict — geometry buys plausibility you can train, on knowledge you never wrote down, at the price of certainty you can no longer have; the mirror image of Volume 2's verdict.
• Filtered MRR — the mean of reciprocal ranks over ranking queries with other known-true answers removed; the volume's headline lift is $0.7778$ against the frozen-random control's $0.1062$ (the analytic chance level on this graph is $0.2543$).
• Soundness probe — an empirical confusion table comparing geometric subsumption ($\lVert \mathbf{c}_A - \mathbf{c}_B \rVert + r_A \le r_B + \varepsilon$) against the exact classifier's entailments; a measurement, never a theorem.
• No model, no guarantee — zero loss would make the geometry a model of the ontology, hence one that satisfies every entailment (recall, not precision); at any nonzero loss ($0.6848$ for balls, $0.0678$ for boxes) the guarantee does not exist.
• Algebraic ceiling — a limitation provable for every parameter setting of a family: DistMult's forced tie $s(h, r, t) = s(t, r, h)$, the ball's false-positive lens cover, the 1-WL bound on message passing.
• Autograd oracle — an independent implementation (torch.autograd) that recomputes the suite's three core loss gradients (the TransE margin hinge, the DistMult logistic loss, the box inclusion hinge) and must agree to tolerance; the calculus analogue of Volume 2's HermiT check. Beyond those three families, only bilinear.py and attention_demo.py carry in-module central-difference checks; the remaining manual gradients are vouched for by competency outcomes alone.
• Competency ledger — validate.py's 15 named checks, one per load-bearing claim, whose exit code is the volume's acceptance verdict: 15/15.
• The five tensions — exact vs robust, proof vs score, discrete vs differentiable, constructed vs learned, closure vs capacity: the axes on which every integration method must declare its position.

Where this leads

The two columns are written, and this volume's methods can only choose between them. The next volume stops choosing. Volume 4 — Neuro-Symbolic Integration builds the machinery that lets gradients flow through logic itself: semantic loss functions that differentiate the probability of a constraint being satisfied, weighted model counting that turns logical structure into an arithmetic circuit a gradient can traverse, and differentiable query answering that executes the query plan inside the network. Every device there will be graded by the ledger built here: the gold standard stays runnable, the probes stay adversarial, and the question stays the same — how much of the left column's guarantee can survive contact with the right column's training loop.