The Eight Claims: C1–C8 and the Wedge

📍 Where we are: Part VII · The SATORI Capstone — Chapter 20. The SATORI Architecture assembled the operator, its two substrates, and the trace discipline, and paired four claimed properties with four instruments. This chapter widens the ledger to the program's full contract: eight claims, each written as an experiment before anything was built, and the committed table that says which of them a desk can already grade.

A research program is a bet, and a bet only means something if its terms are written down before the outcome is known. SATORI's terms are a claims-to-experiments matrix: eight numbered claims, C1 through C8, each frozen with its experiment, its baseline family, and its metric before implementation began, so that no result can be quietly reframed as what the program "really meant." This chapter does two things with that matrix. First, it evaluates the largest honest subset a thirteen-entity desk can evaluate: the companion's satori_eval.py commits real numbers for C1, C2, C3, C5, and C8, and prints C4, C6, and C7 as cited-only with the reason each one cannot be graded here. Second, it assembles the wedge: the related-work argument that the eight claims jointly name a corner of design space no existing family occupies, which is the program's reason to exist and, read soberly, nothing more than that. The chapter's centerpiece is a table the code prints, not a story the prose tells.

The simple version

Imagine a pool player who announces, before every shot, exactly which ball goes in exactly which pocket. Announced shots that land count; lucky slop does not, no matter how good it looks. Now imagine the player also hands you a scorecard before the game listing eight announced shots, and next to three of them a note: "cannot be attempted on this table; here is the table it needs." That scorecard is this chapter. The eight claims are the announced shots, the committed evaluation script is the referee who watched them land or miss, and the three honest notes are the claims that need hardware, scale, or a second ontology this desk does not have. What makes the whole thing trustworthy is the order of events: the announcements came first.

What this chapter covers

• Claims as contracts: why a research program should publish its claims-to-experiments matrix before building anything, and the eight claims stated one by one, each in a single sentence with its metric and its baseline family named.
• The evaluation harness: how satori_eval.py wires one instrument from each earlier Part of this volume to the claim it grades, and the honesty-flag mechanism that stamps every row toy-verified or cited-only.
• The five graded claims, read in full: C1's committed MRR (mean reciprocal rank) and where its recall actually comes from; C2's planted-rule recovery with the router gradient derived step by step; C3 and C8 as the soundness pair the symbolic pillar demands; C5's calibration and abstention numbers with Part II's identifiability caveat stapled on.
• The three cited-only claims: C4, C6, and C7, each with the printed reason it cannot be graded at desk scale and an evidence plan precise enough that a reader could referee a future result.
• The wedge: the three related-work families tabulated by which corners they hold, the empty conjunction the eight claims map onto, and the sober reading that a wedge is an opportunity argument, never a result.

Claims as contracts

Why freeze a claims matrix before writing a line of code? Three reasons, each of them a discipline the field mostly lacks. Falsifiability: a claim with a named metric and a named baseline can lose. "The attention operator answers multi-hop queries competitively" is a slogan; "filtered MRR per query type against the query-embedding baseline family" is a bet that a specific number can refute. Scope discipline: the matrix decides in advance what evidence would count, so a promising side result cannot drift into the headline and a disappointing main result cannot be demoted to an ablation. Every experiment either serves a numbered claim or is not run. Reviewer fairness: a reader handed the matrix can audit the paper against the program's own stated terms rather than against terms reconstructed after the fact. The SATORI outline states the rule in one sentence: every claim must map to an experiment, a baseline set, and a metric before implementation, so no experiment is wasted.

Here are the eight, each in one sentence, with the metric and the baseline family the matrix names. C1 (multi-hop answering): the symbolic-attention operator answers multi-hop EPFO queries (existential positive first-order queries: projections, intersections, unions) competitively with the query-embedding line, measured by filtered MRR and Hits at 1, 3, and 10 per query type against the Query2Box, BetaE, GQE, and GNN-QE/CQD family [1]. C2 (rule learning): attention routing learns correct rules without enumerating the rule space, measured by rule precision and recall and by recovery-at-k against the differentiable rule-mining line of Neural-LP, TensorLog, DRUM, and NTP/GNTP [2]. C3 (faithful proofs): the discretized proof trace re-verifies as a genuine minimal justification, measured by erasure sufficiency and comprehensiveness and by proof-verify rate against attention-rollout and gradient-saliency explainers [3]. C4 (throughput): GPU-batched inference beats CPU symbolic engines, measured by queries per second, latency, and memory scaling curves against PyReason, Scallop, and DeepProbLog. C5 (calibration and abstention): interval annotations yield calibrated confidence and useful abstention, robust to reasoning shortcuts, measured by ECE (expected calibration error), risk-coverage curves, and a shortcut-rate probe against a plain softmax head with temperature scaling [4]. C6 (grounding helps): ontology grounding measurably improves answering, measured by the MRR change in on/off ablations against the system's own ungrounded variant. C7 (transfer): learned reasoning transfers across ontologies zero- and few-shot, measured by MRR under transfer against per-ontology retrained baselines, RRN chief among them. C8 (crisp soundness): classical soundness is recovered as the temperature vanishes, measured by entailment agreement (precision and recall) against a reference EL reasoner such as ELK or HermiT and against the Datalog least fixpoint.

Notice the grain of the sentences. None says "our system is interpretable" or "our system is scalable"; each names the quantity that would be measured, the family that would be beaten, and implicitly the experiment that could fail. That grain is what makes the rest of this chapter possible: five of the eight sentences are precise enough that a thirteen-entity knowledge base, armed with the instruments this volume has already built and validated, can grade them today.

The contract and its grading: eight pre-registered claims, five graded by instruments built in earlier Parts, three stamped cited-only with printed reasons, and the wedge naming the corner no existing family holds. Original diagram by the authors, created with AI assistance.

The harness: the volume's toolbox, enumerated

The evaluation script is deliberately unoriginal. satori_eval.py builds almost nothing; it wires. Its toolbox is the volume's: the kernel and its two classical oracles from Symbolic Attention (satori_lite, which itself imports Volume 1's forward chainer and Volume 2's EL completion), the minimal-justification oracle from Part I's Justifications chapter (justifications.py, Reiter's hitting-set tree), the erasure protocol re-applied inline following Part I's Faithfulness chapter, the ECE helper and fitted temperature imported from Part III's Calibration chapter (calibration.py), the abstention policy re-implemented inline after Part III's Abstention chapter, and Volume 4's 36-query bank (the nine EPFO types plus the five negation types) with its filtered-ranking protocol (query_dag.py, cqd.py). Every instrument that grades a claim here was built, derived, and committed in an earlier chapter against systems that were not SATORI. The harness's one structural idea is the honesty flag: the claims table it prints carries a status column, and every row is stamped either toy-verified, with the committed number as evidence, or cited-only, with the reason grading is impossible at this scale. The table is data in the code, not prose (satori_eval.py lines 628–649):

    rows = (
        ("C1 multi-hop EPFO answering", "toy-verified",
         f"MRR {mrr['godel']['mrr']:.3f} vs random {mrr['random']['mrr']:.3f}"
         " / oracle 1.000"),
        ("C2 router learns rules", "toy-verified",
         f"advises∘advises recovered, α = {out['alpha'][out['top']]:.3f}, "
         "exact decode"),
        ("C3 faithful proof traces", "toy-verified",
         f"comp {out['n_broke']}/{out['n_del']}, suff 4/4, trace ⊇ MinA 2/2"),
        ("C4 GPU-batched scalability", "cited-only",
         "proxy gpu_fixpoint.py; needs PyReason/Scallop at scale"),

Every evidence string interpolates a variable the run() function computed and asserted seconds earlier; a regression in any number breaks the run before the table prints. The world being graded is the same one the whole series has carried: 13 entities, a training graph of 15 edges inside a full graph of 18, and the 36-query bank spanning 14 query types. The header states the scope and the split of the verdicts up front:

SATORI-eval: the eight claims at toy scale (honest subset of the claims matrix)
  world  : 13 entities; G_train 15 ⊂ G_full 18 edges; bank 36 queries / 14 types
  claims : C1/C2/C3/C5/C8 toy-verified below; C4/C6/C7 cited-only (see the table)

One phrase in that header deserves weight: honest subset. Nothing in this chapter is evidence at benchmark scale, and the harness never pretends otherwise. What the desk can establish is that the mechanisms exist and behave as claimed on a world small enough to check exhaustively; what it cannot establish, it names.

C1 in full: the kernel on the query bank

C1 asks whether the operator built for soundness can also answer: run the kernel not to closure but along a query's computation DAG, and score it under the protocol the query-embedding literature standardized [1]. The evaluator is thirty lines (satori_eval.py lines 119–151): an anchor entity becomes a one-hot degree vector over the 13 entities, a projection along role $r$ is the kernel's own message pass, $v'[t] = \mathrm{softmax}_h\, \mathrm{softmin}(v[h],\, M_r[h,t])$ (read: an entity $t$ is reached to the degree that some source $h$ is both active and connected, with the softmax merging alternative sources and the softmin conjoining "active" with "connected"), intersection is softmin, union is softmax. Here $M_r \in [0,1]^{13 \times 13}$ is the soft adjacency for role $r$, the matrix whose entry $M_r[h,t]$ is the degree of the edge $r(h,t)$; $v \in [0,1]^{13}$ is the running answer-degree vector. The chapter before this one built $M$: Volume 3's ComplEx scores $s$ (from the embedding of dimension $d = 16$) read through the calibrated sigmoid $\sigma(s/\tau^\ast)$, where $\tau^\ast = 1.4172$ is Part III's fitted temperature, and every observed training edge pinned to exactly $1.0$ (satori_eval.py lines 102–116).

Before any soft number is trusted, the harness runs the crisp leg: on the hard 0/1 training adjacency at vanishing temperature, the thresholded kernel must return exactly the symbolic executor's answer set on all 36 queries of all 14 types, negation included (lines 424–431, an assert, not a statistic). Only then does the soft ranking run. The metric is filtered MRR (mean reciprocal rank): for each hard answer, an entity that answers the query on the full 18-edge graph but that no traversal of the 15-edge training graph can reach, rank all entities by degree with the other true answers removed from the candidate list, take the reciprocal of the hard answer's rank, and average. In symbols, with $H$ the set of (query, hard answer) pairs and $\mathrm{rank}(q,a)$ the filtered rank,

$$\mathrm{MRR} \;=\; \frac{1}{|H|} \sum_{(q,a)\, \in\, H} \frac{1}{\mathrm{rank}(q,a)}, \qquad |H| = 17$$

over the nine negation-free query types. Two labels in the table below need a key. The kernel row says Gödel because the run uses the previous chapter's default min/max semantics, softmin as the conjunction and softmax as the disjunction. The per-type codes are Volume 4's naming and read digit-then-operation: 1p, 2p, and 3p are chains of one, two, and three projection hops, 2i and 3i are two- and three-way intersections, pi is a projection feeding an intersection, ip an intersection feeding a projection, 2u a two-way union, and up a union feeding a projection. The committed table:

[1] C1 — the kernel answers the EPFO bank (filtered MRR, 17 hard answers, 9 ¬-free types)
  τ→0 sanity: thresholded kernel == symbolic executor on all 36 queries (asserted)
  adjacency: M = σ(s/τ*) over ComplEx scores, τ* = 1.4172 (calibration.py); TRAIN edges pinned to 1
  G_train traversal (symbolic)    0.1488   0 on every hard answer BY DEFINITION
  random scorer (seed 0)          0.2301   the uninformed floor
  SATORI kernel (Gödel, τ=0.01)   0.5680   the C1 number
  G_full oracle                   1.0000   ceiling; the honest gap is real
  kernel per type: 1p 0.538  2p 0.538  3p 0.545  2i 0.583  3i 0.750  pi 0.667  ip 0.111  2u 0.600  up 0.550

Now the honest position of $0.568$. It is not a leaderboard entry, and three features of the table say so. First, the floor is high: with only 13 candidate entities, a random ranking already earns $0.230$, so toy MRRs must never be compared with benchmark MRRs computed over tens of thousands of candidates. Second, the harness asserts a window, not just a victory: the kernel must beat the random floor by at least $0.25$ and the traversal baseline by at least $0.30$, and it must also stay below $0.8$ (lines 448–450), because a near-oracle score from a $d=16$ toy imputer would signal leakage, not brilliance. Third, the per-type row shows where the recall comes from and where it dies: the purely symbolic traversal scores every hard answer zero by definition (a hard answer is precisely what traversal cannot reach), so every point of the kernel's $0.568$ is contributed by the calibrated neural adjacency imputing held-out edges inside the kernel's own algebra, and the weakest cell, ip at $0.111$, is the type whose intersection sits before its projection, so an imputation error entering the intersection is then propagated rather than averaged away. What the toy CAN show, and does show, is the mechanism: an exactness-first kernel, unchanged from the one that recovers two classical closures, answering compositional queries at all, with its neural half confined to the leaf matrices. Whether the same mechanism is competitive on the baseline family's own benchmarks is exactly what the matrix says it is: a claim, awaiting the experiment at scale.

C2 in full: the planted rule and the router gradient

C2 is the learnability claim, and it is graded by the cleanest protocol available: hide a rule, then check whether training recovers it exactly. The hidden rule is Volume 1's grandAdvisor(x,z) ← advises(x,y) ∧ advises(y,z). The hypothesis space is every length-2 role chain over the 5 base roles: $25$ templates, template $k = (r,s)$ meaning "$r$ then $s$." For each, the harness precomputes the kernel's chain message over the full graph, $C_k[x,z] = \mathrm{softmax}_y\, \mathrm{softmin}(A_r[x,y],\, A_s[y,z])$, where $A_r$ and $A_s$ are the crisp 0/1 adjacency matrices of roles $r$ and $s$ over the full 18-edge graph (the hard counterpart of C1's soft $M_r$): a $13 \times 13$ matrix per template, constant with respect to training (satori_eval.py lines 166–179). This is the path-matrix reading of a chain rule that the differentiable rule-mining line introduced, precomputed here per template because 25 templates fit on a desk [2]. The only trainable object is a router: a logit vector $\mathbf{w} \in \mathbb{R}^{25}$ (one real number per template) passed through a softmax to give attention $\alpha_k = e^{w_k} / \sum_j e^{w_j}$, and a prediction that mixes the templates, $P[x,z] = \sum_k \alpha_k\, C_k[x,z]$. Supervision is minimal and rule-free: the grid $G \in \lbrace 0,1 \rbrace^{13 \times 13}$ with a $1$ on exactly the 3 gold grandAdvisor pairs from the Volume 1 closure and $0$ elsewhere (lines 454–458). The router is never shown a rule, a template label, or a trace; it sees answers.

The loss is the mean cross-entropy over all $N_{\text{cells}} = 13 \times 13 = 169$ cells (the count gets its own symbol so it cannot collide with the adjacency matrix $M$), with a guard $\varepsilon = 10^{-6}$ inside each logarithm to keep it finite:

$$L \;=\; -\frac{1}{N_{\text{cells}}} \sum_{x,z} \Big[ G_{xz} \ln\!\big(P_{xz} + \varepsilon\big) + (1 - G_{xz}) \ln\!\big(1 - P_{xz} + \varepsilon\big) \Big].$$

The gradient is derived by hand in three links, because this chapter owns the math it commits. Link one, loss to prediction: differentiating each term of $L$ with respect to the single cell $P_{xz}$ it mentions, $\frac{\partial}{\partial P}\ln(P+\varepsilon) = \frac{1}{P+\varepsilon}$ and $\frac{\partial}{\partial P}\ln(1-P+\varepsilon) = \frac{-1}{1-P+\varepsilon}$, so

$$\frac{\partial L}{\partial P_{xz}} \;=\; -\frac{1}{N_{\text{cells}}}\left[ \frac{G_{xz}}{P_{xz}+\varepsilon} \;-\; \frac{1-G_{xz}}{1-P_{xz}+\varepsilon} \right].$$

Link two, prediction to attention: $P_{xz}$ is linear in $\alpha_k$ with coefficient $C_k[x,z]$, so the chain rule sums over every cell the attention touches,

$$g_k \;\equiv\; \frac{\partial L}{\partial \alpha_k} \;=\; \sum_{x,z} \frac{\partial L}{\partial P_{xz}}\, C_k[x,z].$$

Link three, attention to logits, through the softmax Jacobian $\frac{\partial \alpha_j}{\partial w_i} = \alpha_j(\delta_{ij} - \alpha_i)$, where $\delta_{ij}$ is the Kronecker delta, equal to $1$ when $i = j$ and $0$ otherwise (Volume 3's attention chapter derived this entry by the quotient rule). Contract it against $g$:

$$\frac{\partial L}{\partial w_i} \;=\; \sum_j g_j\, \alpha_j (\delta_{ij} - \alpha_i) \;=\; g_i \alpha_i \;-\; \alpha_i \sum_j \alpha_j g_j \;=\; \alpha_i \Big( g_i - \bar{g} \Big), \qquad \bar{g} \equiv \sum_j \alpha_j g_j,$$

where the first equality split the sum at the delta (only $j = i$ survives the $\delta_{ij}$ term) and the second factored out $\alpha_i$. The closed form is the whole story of attention-based rule learning in one line: each template's logit moves in proportion to its current attention times how much better its gradient signal $g_i$ is than the attention-weighted average $\bar{g}$. Templates that explain the answers better than the current mixture pull attention toward themselves; the rest decay. The committed code is this algebra verbatim (satori_eval.py lines 195–202):

    ex = np.exp(w - w.max())
    alpha = ex / ex.sum()
    P = np.tensordot(alpha, feats, axes=1)
    L = -float(np.mean(G * np.log(P + EPS) + (1 - G) * np.log(1 - P + EPS)))
    dP = -(G / (P + EPS) - (1 - G) / (1 - P + EPS)) / G.size
    g = np.tensordot(feats, dP, axes=([1, 2], [0, 1]))
    gw = alpha * (g - float(alpha @ g))
    return L, gw, alpha

Trust, then verify: before training, the harness compares this hand gradient against central finite differences in all 25 coordinates at the uniform router and demands agreement below $10^{-8}$ (lines 460–466). Then plain gradient descent, $\mathbf{w} \leftarrow \mathbf{w} - \eta\, \partial L/\partial \mathbf{w}$ with learning rate $\eta = 5.0$ for 400 steps from $\mathbf{w} = \mathbf{0}$ (every template at $\alpha_k = 1/25 = 0.04$). The committed trace:

[2] C2 — planted-rule recovery (softmax router over 25 chain templates)
  hidden: grandAdvisor(x,z) ← advises(x,y) ∧ advises(y,z); supervision: its 3 query answers
  hand gradient vs central differences: max error 1.17e-11 over 25 coordinates
  loss: 0.0730 (step 1)  →  0.0658 (step 10)  →  0.0231 (step 100)  →  0.0197 (step 400)
  router attention: advises∘advises 0.9718   advises∘cites 0.0012   cites∘advises 0.0012   (rest ≤ the third)
  decoded rule == the hidden kb rule, exactly (asserted)

Read the trace with a skeptic's eye. The loss starts low ($0.0730$) because $G$ has only 3 positives among 169 cells, so even the uniform mixture is mostly right by predicting small values everywhere; the informative event is not the loss falling but the attention concentrating, from $0.04$ to $0.9718$ on advises∘advises, with the runners-up at $0.0012$. And the pass condition is not merely high attention (an $\alpha > 0.9$ guard on the winner is asserted too, line 472); the decisive check is the exact decode: the argmax template, rebuilt as an IR (intermediate-representation) rule, must equal, tuple for tuple, what compile_horn produces from the hidden knowledge-base rule (lines 467–471). Recovery here is a syntactic identity, not a similarity score.

Now the claim's real content, honestly bounded. The contrast class's hypothesis space is chain rules up to a length bound, a space exponential in that bound; the Neural-LP and DRUM line avoids materializing it (Neural-LP by recurrent attention over relation operators, DRUM by a low-rank factorization of the rule-confidence tensor), and pays for the escape with chain-only rule shapes, a hard length cap, and weak systematic generalization, which is the line's acknowledged wall; NTP is the member that literally enumerates proof paths [2]. At 25 templates, this toy simply materializes the space those systems deliberately factorize; nothing else would be honest to admit. What the desk verifies is therefore the recovery mechanism: gradient descent through the kernel's own softmin/softmax algebra concentrates a router on the planted rule and decodes it exactly. What C2 claims at scale is stronger and remains unproven here: search-free induction, routing over structured template spaces too large to enumerate, with the kernel's algebra replacing the enumeration. The matrix's synthetic-ontology experiments, with controllable depth, branching, and noise, are where that clause gets graded.

C3 and C8: the soundness pair

Two claims anchor the program's identity, and it is worth saying why before reading their numbers. Strip C3 and C8 away and SATORI is one more neural query answerer with an attention map; keep them and it is a reasoner that learned: whatever the neural half does, the crisp limit is a classical closure (C8) and the derivation record is a checkable proof (C3). These are the symbolic pillar's guarantees, the ones the neural pillar is being asked to keep. They are also, not coincidentally, the cheapest rows of the matrix to grade at toy scale, for one structural reason: oracles exist, because this series built them. Volume 1's forward chainer computes the exact Horn closure, Volume 2's completion algorithm computes the exact EL closure, and Part I's justifications.py enumerates every minimal justification by Reiter's hitting-set tree. A claim is exactly as cheap to verify as its ground truth is to compute, and for these two the ground truth is a solved problem at thirteen entities.

C8 is graded first, because everything else stands on it. The harness re-invokes the previous chapters' entire assert suite and re-checks its headline equalities (satori_eval.py lines 417–419):

    sat = satori_lite.run()
    assert len(sat["closure"]) == 47 and len(sat["el_closure"]) == 46
    assert sat["recall"][3][0][1] == sat["recall"][3][1][1] == 1.0  # L ≥ D = 3

Decoded: at vanishing temperature the thresholded kernel state equals, as a set, the 47-atom Horn closure and the 46-atom EL closure, and recall reaches exactly $1.0$ at depth $L = 3$, the joint saturation depth. This is entailment agreement with the reference reasoners at precision and recall $1.0$, the matrix's C8 metric, on the one knowledge base where exhaustive agreement is checkable. The claims table row compresses it to Horn 47/47, EL 46/46, complete iff L ≥ 3.

C3 is graded by two independent instruments, one per face of the running example. The first is Part I's erasure protocol [3], strengthened for a deterministic reasoner: where ERASER deletes the whole rationale and watches the confidence drop, here a trace is graded comprehensive only if deleting each fact it cites, one at a time, breaks the conclusion (per-fact necessity, the justification chapter's condition), and sufficient if the cited facts alone re-derive it, which is the ERASER clause unchanged. The harness collects the base-fact leaves of four derived atoms' traces, then re-runs the kernel with facts zeroed at the input, the model untouched (satori_eval.py lines 237–251). The second instrument is Part I's justification oracle: rebuild the EL instance so that every compiled rule remembers which original axiom produced it (lines 290–319), read the discretized trace of a subsumption as the set of axiom identifiers appearing anywhere in its derivation tree, and demand that this set contains a true MinA, a subset-minimal axiom set entailing the subsumption, as found by the hitting-set tree. Both verdicts commit:

[3] C3 — faithful traces: erasure + MinA containment
  Horn face, 4 derived atoms — e.g. grandAdvisor(alice, carol) has trace leaves advises(alice, bob), advises(bob, carol)
    comprehensiveness 8/8: every leaf deletion kills its atom; leaves ALONE re-derive it (4/4)
    12 seeded non-trace deletions (default_rng(5)): nothing breaks (asserted)
  TBox face — the discretized trace vs justifications.py:
    Professor ⊑ Researcher: trace axioms {1} ⊇ MinA {1}   (all MinAs: {1} {4, 5})
    TenuredStudentAdvisor ⊑ ⊥: trace axioms {6, 10, 11, 12} ⊇ MinA {6, 10, 11, 12}   (all MinAs: {6, 10, 11, 12})

Every one of the 8 leaf deletions kills its atom, the leaves alone re-derive all 4 atoms, and 12 seeded control deletions of non-trace facts change nothing: comprehensiveness and sufficiency both at $1.0$, against a protocol under which Part I showed ordinary attention weights fail. On the TBox face, note the wording the previous chapter fixed and this one keeps: the trace contains a MinA, it need not be one. Professor ⊑ Researcher has two MinAs, and the trace carries whichever derivation won the argmax; the unsatisfiability proof happens to be its own unique MinA, so there containment is equality. The matrix's C3 sentence, "the discretized trace re-verifies as a genuine minimal justification," is graded here in its precise form: a certified minimal proof can be extracted from the trace by intersection with the oracle's output, because the trace provably covers one (lines 505–510). Cheap to state, cheap to check, and the entire reason the word "faithful" in this program is a theorem-shaped claim rather than a vibe.

C5 with Part II's caveat stapled on

C5 has three clauses: the annotations are calibrated, they support abstention, and the package is robust to reasoning shortcuts. The desk grades the first two and has something honest to say about why it cannot grade the third.

Calibration first. The kernel's query degrees are read as confidences and scored by Part III's instrument, the expected calibration error [5]: sort the $N$ predictions into $B$ equal-width confidence bins, and compute $\mathrm{ECE} = \sum_{b=1}^{B} \frac{n_b}{N}\, \lvert \mathrm{acc}(b) - \mathrm{conf}(b) \rvert$, where $n_b$ counts the predictions in bin $b$, $\mathrm{acc}(b)$ is the fraction of them that are true, and $\mathrm{conf}(b)$ is their mean stated confidence; zero means the stated numbers are honest frequencies. The population is every (query, entity) pair that actually needs imputation, meaning the entity is not already a traversal answer: 306 pairs across the nine negation-free types, of which exactly the 17 hard answers are true (satori_eval.py lines 513–523). The committed number is $\mathrm{ECE} = 0.0186$, under the asserted $0.05$ bar; the kernel's degrees are usable confidences here, and the credit belongs largely to Part III's temperature $\tau^\ast$, fitted by temperature scaling [4], already being inside the adjacency.

Abstention is where the architecture's interval annotation earns its keep. Each query is evaluated twice, as an answer-set pair $[\ell, u]$: the lower set from the observed training edges alone (what is derivable), the upper set from a 62-edge typed completion containing every edge whose endpoint concepts match a pattern the training graph exhibits for that role (what is possible), with an unasserted atom defaulting to the full interval, the open-world unknown (lines 334–376). The decision policy answers YES inside the lower set, NO outside the upper set, and abstains in the gap. Scored over all $36 \times 13 = 468$ decisions of the full bank:

[4] C5 — calibration + open-world abstention
  kernel degrees on the 306 imputation-needing (query, entity) pairs: ECE = 0.0186
  interval [ℓ, u]: ℓ from G_train, u from the 62-edge typed completion (⊇ all 18 true edges)
  policy                    coverage   acc-on-answered
  closed-world traversal      1.0000   0.9487   (24 errors = 23 hard answers + the 2in witness)
  interval + abstain          0.8205   1.0000   (19 yes + 365 no; abstains 84/468)
  witness affiliated(dave,x) ∧ ¬affiliated(erin,x): the closed world answers cmu — WRONG on
  G_full; the interval reads cmu as unknown [0,1] and abstains (the open-world default)

Work the row. The closed-world policy answers everything (coverage $1.0$) and errs 24 times, so its accuracy is $(468 - 24)/468 = 0.9487$; its 24 errors are precisely the 23 hard answers of the full bank plus one negation query's witness, where treating "not derived" as "false" manufactures a wrong yes. The interval policy answers $19 + 365 = 384$ decisions, coverage $384/468 = 0.8205$, and every answered decision is correct, an accuracy-on-answered of $1.000$ enforced by assert (lines 528–530). The trade is stated by the numbers themselves: about eighteen percent of decisions are refused, and in exchange nothing answered is wrong, with the harness checking the interval's soundness invariant, lower set $\subseteq$ true answers $\subseteq$ upper set, on every query on the way (line 390). This is Part III's risk-coverage story running on the architecture's own data model rather than on a bolted-on confidence head.

Now the third clause, named honestly as the claim's hardest. The matrix promises robustness to reasoning shortcuts, Part II's phenomenon of models right for the wrong internal reasons. On this desk the clause is nearly vacuous: the toy's concepts are fixed symbols, given, not learned, so there is no concept-extraction layer for a shortcut to hide in, and the shortcut surface is minimal by construction; the counting instruments live in the companion's shortcuts.py and rsbench_lite.py, and Part II's chapters showed on their own ground how many label-consistent wrong concept maps a task can admit. At scale the situation inverts. A deployed SATORI grounds its symbols in learned perception or learned embeddings, and the moment the concept vocabulary is learned, C5 inherits the identifiability problem in full: calibrated degrees over mislabeled concepts are calibrated nonsense, and no ECE computed at the query level can detect it. The claim's own metric list concedes this by including a shortcut-rate probe alongside ECE. C5 is toy-verified in its first two clauses and should be read as conditionally stated in its third; of the five graded claims, it is the one whose grade travels least.

C4, C6, C7: cited-only, with reasons and evidence plans

Three rows of the matrix cannot be graded at a desk, and the harness prints why rather than stretching. The discipline matters as much as the numbers did: a claims table that only ever says "verified" is an advertisement.

C4, throughput, stays with the paper because throughput is a property of hardware plus scale, and this desk has neither. The in-suite artifact is a proxy, not a measurement: Part IV's gpu_fixpoint.py closed a batch of one hundred knowledge-base variants in one stacked dense pass, demonstrating the shape of the win (a fixpoint expressed as regular tensor algebra batches for free) on matrices far too small to exercise an accelerator. The prior art the claim must beat is not naive Python; it is engineered CPU parallelism, and the volume has already quoted its numbers: the RDFox line materialized the LUBM-50K closure, 6.7 billion explicit triples growing to 9.2 billion, at 6.1 million triples per second, with a 128-thread run 69.6 times faster than its own single thread [6]; the neuro-symbolic engines named as C4 baselines (PyReason [7], Scallop [8], DeepProbLog) sit below that line, their symbolic cores CPU-bound. A refereeable positive result is therefore specific: queries per second and latency, as functions of knowledge-base size and query depth, for the batched kernel on real accelerators against those engines on comparable hardware budgets, at matched soundness, with the scaling curve, not a single point, as the exhibit. Materialization versus Rewriting and GPU Reasoning hold the toy's half of this story.

C6, grounding helps, is degenerate at toy scale for a reason worth understanding: the ablation has nothing to turn off. The toy kernel is built from the TBox; its rules are the compiled axioms, so "grounding off" deletes the reasoner rather than ablating a feature. The claim only becomes testable when the system has an ungrounded degree of freedom, embeddings that could ignore the ontology: then the matrix's experiment is exact (initialize from TBox structure versus randomly; run the OWL 2 EL and OWL 2 RL profile objectives separately and together; boxes versus balls; report the MRR difference, self-ablated). The geometric evidence that grounding carries real signal at ontology scale lives with the box-embedding line, Box2EL [9] and TransBox [10], whose containment losses encode TBox structure directly; the toy's contribution was Volume 3's verdict that boxes, not balls, can carry a subsumption order faithfully. A positive C6 is a positive Δ MRR attributable to structure initialization alone, on ontologies the size of GALEN or the Gene Ontology, with the ablation grid published.

C7, transfer, needs a second ontology, and the toy has one world. The claim's contrast is precise: the deep ontology-reasoning line that C7 must improve on answers accurately within a domain but must be retrained per ontology, which is its named limitation [11]. C7 bets that a router and kernel trained on one ontology's rule vocabulary answer zero- and few-shot on another, because what was learned is routing over rule shapes rather than facts about one domain. A refereeable positive result: train on ontology A, freeze, evaluate MRR on ontology B against the retrained-per-domain baseline given B's full training budget, and report the fraction of the retrained performance recovered at zero and at few shots, across ontology pairs of graded vocabulary overlap. Nothing smaller settles it, which is exactly why the row says cited-only.

The committed centerpiece: the claims table

Everything above compresses into the table the harness prints last, the chapter's actual deliverable. Five rows carry committed numbers that asserts guard; three rows carry reasons. It is worth reproducing whole, because its shape, claims down the side, honesty flags in the middle, evidence on the right, is the methodological export of this volume:

[5] the claims table (C4/C6/C7 stay with the paper: stated, not stretched)
  C1 multi-hop EPFO answering   toy-verified  MRR 0.568 vs random 0.230 / oracle 1.000
  C2 router learns rules        toy-verified  advises∘advises recovered, α = 0.972, exact decode
  C3 faithful proof traces      toy-verified  comp 8/8, suff 4/4, trace ⊇ MinA 2/2
  C4 GPU-batched scalability    cited-only    proxy gpu_fixpoint.py; needs PyReason/Scallop at scale
  C5 calibration + abstention   toy-verified  ECE 0.019; coverage 0.821 @ acc-on-answered 1.000
  C6 ontology grounding Δ MRR   cited-only    ablation degenerate here; Box2EL / TransBox carry it
  C7 cross-ontology transfer    cited-only    needs a 2nd ontology; RRN is the failing baseline
  C8 crisp soundness (τ→0)      toy-verified  satori_lite re-run: Horn 47/47, EL 46/46, complete iff L ≥ 3

Five of eight verified at toy scale, three stated and sourced. Read as a report card it is modest. Read as a method, claims first, instruments independent, receipts committed, flags honest, it is the volume's entire argument in fourteen lines of stdout.

The wedge: the empty corner

The eight claims were not chosen by ambition; they were chosen by a map. The program's related-work survey organizes the field into families and tabulates what each one holds and drops, and the pattern that emerges is the wedge: every family covers two or three of the properties the claims name, and no family covers the conjunction. Three families carry the argument:

family	exemplars	holds	misses
exact annotated logic	PyReason [7], ProbLog/DeepProbLog, and classically RDFox [6]	soundness and proofs (C3, C8); annotated open-world semantics in the PyReason line (C5's substrate)	rules are hand-authored, never learned (C2); CPU-bound inference (C4)
differentiable rule learners	Neural-LP, DRUM, NTP [2]	rule learning from answers (C2); GPU-friendly algebra (toward C4)	ontology-blind (C6); chain-only rules under a hard length cap (C2's scale clause); no verified proofs (traces are never re-checked as justifications), no calibration (C3, C5)
ontology embedders / neural ontology reasoners	Box2EL [9], TransBox [10], RRN [11]	geometric TBox grounding (C6); scalable inference (toward C4)	no derivations to check (C3, C8); per-ontology retraining (C7)

The fourth line of the map is the task lineage rather than a design family: the query-embedding systems that own C1's benchmarks answer multi-hop queries competitively and are, by construction, not ontology-grounded, not proof-faithful, and not calibrated for abstention [1]. Lay the eight claims over this table and each claim lands on a hole: C2 on the exact family's, C3 and C8 on the embedders' and the query line's, C4 on the exact family's, C5 on nearly everyone's, C6 on the rule learners', C7 on RRN's. The conjunction of all eight is the corner no row reaches, and SATORI's wedge is precisely the assertion that one operator over an annotated, box-carried substrate can stand there.

Now the sober reading, because a wedge argument has a failure mode: mistaking the existence of a gap for evidence that the gap is fillable. The gap being real is a fact about the literature; filling it is a bet about the world. Corners can be empty because nobody tried, or because the properties trade against each other: exactness against learnability, batching against interval semantics, transfer against grounding. The desk's own numbers already hint at the tensions (the next section makes them explicit), and the program's gap map, eight named gaps G1 through G8 running from the exact-versus-learnable split to meta-cognition, is honest about how much of the corner remains unoccupied even after this chapter's receipts. That map is the Open Problems chapter's syllabus, which is the correct address for it: an opportunity argument belongs at the start of a research program, and open problems belong at the end of a textbook.

The unsolved part

The matrix has rows and no interaction terms, and the interactions are where the program will actually be decided. C2 and C3 pull against each other: C3's grades were earned by a kernel whose rules were given, but C2's whole point is that training chooses them, and nothing yet certifies that a router trained for answer accuracy keeps producing traces whose discretization contains a MinA. The harness itself keeps the two experiments separate, trace probes on the frozen kernel, recovery on the router, precisely because the joint test does not exist yet. C4 and C5 pull the same way: batched throughput wants one scalar degree per atom flowing through dense kernels, while C5's abstention needs two interval endpoints and a typed upper bound built from symbolic signatures, so every systems optimization that flattens the interval to its lower end quietly deletes the open world that C5's accuracy-on-answered of $1.000$ was purchased with. A complete contract would carry rows like "C2 training preserves C3 faithfulness, measured by re-running erasure and MinA containment on the trained system," and the matrix, as frozen, has none. The wider unsolved part is normative: pre-registered claims matrices of this kind remain rare for architecture papers, where the claims are usually reverse-engineered from whatever the experiments delivered. The chapter has no theorem to offer there, only the demonstrated cost of the alternative discipline: a few dozen lines of table-printing code and the willingness to write "cited-only" three times.

Why it matters

This chapter is the volume working as designed, once, end to end. Every instrument that graded a claim was built earlier against other systems: erasure in Part I, justifications in Part I, ECE and abstention in Part III, the batching proxy in Part IV, the query bank in Volume 4, the oracles in Volumes 1 and 2. The capstone architecture then arrived and was scored, not admired, and where the instruments could not reach, the table said so in print. For the reader heading into research, the transferable object is not SATORI; it is the contract form. Before building, write each claim as one sentence with a metric and a baseline family; wire an evaluation that prints a status flag per claim; let "cited-only, because" be a legal and unembarrassing value of that flag. A program written this way can be refereed by a stranger, inherited by a successor, and falsified by its own harness, which are three definitions of the same virtue. And the five toy receipts, whatever they fail to prove about scale, prove one thing exactly: the eight sentences are operational, each one already attached to code that could grade it, which is more than most architecture claims can say on the day they are made.

Key terms

• Claims-to-experiments matrix: a pre-registered table mapping every claim of a research program to an experiment, a baseline family, and a metric, frozen before implementation.
• Honesty flag (toy-verified / cited-only): the status column of the committed claims table; toy-verified rows carry an asserted number, cited-only rows carry the printed reason grading is impossible at desk scale.
• Hard answer: an entity that answers a query on the full graph but is unreachable by traversal of the training graph; the population over which filtered ranking metrics are computed.
• Filtered MRR (mean reciprocal rank): the average of $1/\mathrm{rank}$ over hard answers, with other true answers removed from each ranking; this chapter's C1 metric.
• Planted-rule recovery: the C2 protocol: hide a known rule, train from its query answers alone, and require the learned model to decode back to the hidden rule exactly.
• Exact decode: the pass condition that the router's argmax template, rebuilt as an IR (intermediate-representation) rule, be tuple-identical to the compiled hidden rule; recovery as syntactic identity rather than similarity.
• Discretized trace: the set of original axiom identifiers appearing anywhere in a derived atom's recorded derivation tree; C3 requires it to contain a true MinA.
• MinA (minimal axiom set / justification): a subset-minimal set of axioms entailing a given consequence; enumerable at toy scale by the hitting-set tree.
• ECE (expected calibration error): the bin-weighted average gap between stated confidence and realized accuracy, $\sum_b (n_b/N)\lvert \mathrm{acc}(b) - \mathrm{conf}(b)\rvert$.
• Interval annotation $[\ell, u]$: per-atom lower and upper degrees, derivable versus possible, with the unknown as the full interval; the substrate of C5's abstention policy.
• Coverage / accuracy-on-answered: the fraction of decisions a selective policy answers, and its accuracy on exactly those; the committed C5 pair is $0.8205$ at $1.000$.
• Wedge: a related-work argument locating an empty conjunction of properties no existing family covers; an opportunity claim, never a result.

Where this leads

The wedge said the corner is empty; the receipts said five-eighths of the path to it exists at toy scale; the interaction worries said the remaining path is not a straight line. What remains is to name what the field, not just this program, does not know how to do. Open Problems takes the gap map G1 through G8 that the related-work survey drew, from the exact-versus-learnable split, through rule-search explosion, CPU-bound inference, ontology-blind learning, and non-transferability, to explanation faithfulness, calibration under shortcuts, and meta-cognition, and treats each gap the way this chapter treated each claim: stated precisely, tied to the instrument that would measure progress, and graded honestly on how far anyone has gotten.

---

Companion code: examples/frontier/satori_eval.py wires the volume's instruments to the claims matrix: the kernel and oracles from satori_lite.py, the query bank and filtered protocol from Volume 4's query_dag.py and cqd.py, ECE and the fitted temperature from calibration.py, and the MinA oracle from justifications.py. Run python3 examples/frontier/satori_eval.py to reproduce every number in this chapter, the claims table included; the run is deterministic, and every toy-verified row is guarded by an assert.