Symbolic Attention: Reasoning as a Single Burst

📍 Where we are: Part VII · The SATORI Capstone — Chapter 18. The Entailment-Benchmark Gap closed Part VI by measuring how rarely benchmarks force real entailment; Part VII now builds the operator this entire series has been assembling one volume at a time, and holds it to the standards the previous seventeen chapters set.

Every volume of this series built one half of a machine without ever naming the whole. Volume 2 supplied rules that fire in waves; Volume 3 supplied attention, a differentiable way to weigh alternatives; Volume 4 supplied a semantics under which weighing alternatives is logic. This chapter bolts the parts together into symbolic attention: a reasoner whose entire state is a matrix of degrees, whose single layer fires every completion rule simultaneously as three kinds of attention, and whose network is a fixed stack of that one layer, weight-tied and unrolled, with no halting test and no firing schedule. The construction would be a metaphor if it stopped there. It does not stop there. The companion module examples/frontier/satori_lite.py earns each clause of the claim with an assert: the crisp limit recovers Volume 1's 47-atom Horn closure and Volume 2's EL classification exactly, set equality against both oracles; the recall-versus-depth table reproduces Part IV's truncation law with soundness checked at every depth; and the attention trace behind every derived atom is rebuilt into a derivation that a proof checker verifies rule application by rule application. The chapter's burden is stated up front: make the fusion exact, make it checkable, and price it honestly.

The simple version

Imagine a giant spreadsheet. Every cell holds a number between 0 and 1 saying how strongly some fact is believed, and every cell has the same formula: look at what the other cells said on the last tick, combine the ones my rule needs (taking roughly the weakest), and if several rules propose me, keep roughly the strongest offer. Now press "recalculate" exactly three times. No cell waits for another; the whole sheet updates in lockstep, and three ticks later the sheet holds everything the rules could ever conclude, because in this world no conclusion ever needs more than three steps of ancestry. Better still, every cell quietly wrote down which cells it read, so you can audit any conclusion back to the original entries. Symbolic attention is that spreadsheet: the formula is a completion rule, the "roughly weakest / roughly strongest" dial is attention's temperature, the three ticks are the network's layers, and the audit column is a machine-checkable proof.

What this chapter covers

• The convergence: what Volumes 2, 3, and 4 each contributed, and the fusion claim stated plainly: completion rules, rendered as attention, over Gödel degrees.
• The state before the operator: the soft label matrix $S$ and the per-role soft adjacencies $R_r$, what "soft" means here (Gödel degrees, not probabilities), and the crisp special case that anchors everything.
• One layer, three attentions: conjunction as a temperature-controlled softmin over premises, competition between derivations as a softmax over rules, role composition as a message pass over soft edges, each formula derived and then quoted from the committed code.
• Why lockstep is legal: the monotonicity of the completion operator makes firing order irrelevant, so all rules can fire every layer with no schedule and no convergence test, at the stated price of completeness below the diameter.
• Crisp recovery, both oracles: at temperature near zero the kernel's thresholded state equals the Volume 1 forward-chain closure and the Volume 2 EL classification exactly, both asserts committed.
• The truncation law and the trace: recall rises with depth and completes exactly at $L = 3$, the academic world's derivation diameter, with soundness asserted at every depth; and the recorded argmax parents reconstruct a derivation of grandAdvisor(alice, carol) that a checker verifies step by step.
• The honest burst: on the PTIME-complete (polynomial-time-complete) core, "a single burst" means bounded-depth salience with $L$ chosen in advance, not zero-depth insight.

The convergence, told as the series' own account

Volume 2 contributed the rules. The completion-rules chapter reduced every EL TBox to a handful of normal forms and gave a saturation procedure, CR1 through CR⊥ plus the role-chain rule (CRχ), whose bodies read labels and edges and whose heads write labels and edges, polynomial-time, sound, and complete [1]. Volume 3 contributed attention: relevance-weighted aggregation, and a softmax whose temperature dials it between a hard argmax and a uniform blur [2]; this chapter borrows the transformer's fixed-depth stack of layers and adds a discipline of its own, tying the weights so that one layer, repeated, is the whole network. Volume 4 contributed the semantics that lets the first two meet: put a degree in $[0, 1]$ on every atom, read conjunction as the Gödel t-norm (the minimum), read disjunction as the Gödel t-conorm (the maximum), and the resulting many-valued logic is not a heuristic but a theorem-bearing system whose crisp fragment is classical logic [3].

The fusion claim is this: the completion procedure and the attention stack are the same operator. A rule body that takes the minimum over its premises is attention over premises with the temperature turned down; merging rival derivations of the same head by maximum is attention over rules; propagating a label across a role edge is a message pass over a soft adjacency. The ancestral version of this fusion ran the other direction: differentiable proving grafted soft scores onto backward chaining, searching a proof tree whose branching repeats at every depth [4]. Symbolic attention replaces the search with saturation: no goal, no backtracking, every rule firing everywhere at once, which is exactly the move that makes a fixed parallel stack possible. The name of the source project, SATORI (Symbolic ATtention Over Ontological Reasoning and Inference), takes this chapter's title seriously, and the chapter will return at the end to how seriously the physics permits.

The state: what the reasoner holds between layers

Decode the state before the operator touches it. Fix a finite set of nodes (the things reasoning is about), a finite set of label names (unary predicates or concept names), and a finite set of role names (binary predicates). Write $n$ for the number of nodes and $m$ for the number of labels. The reasoner's entire state is:

• the soft label matrix $S \in [0,1]^{n \times m}$, one row per node, one column per label, where the entry $S[x, A]$ is the degree to which label $A$ holds of node $x$; and
• one soft adjacency matrix $R_r \in [0,1]^{n \times n}$ per role $r$, where $R_r[x, y]$ is the degree to which the edge $r(x, y)$ holds.

Here $[0,1]^{n \times m}$ means the set of $n$-by-$m$ grids of real numbers, each entry between 0 and 1 inclusive, and the symbol $\in$ reads "is a member of": $S$ is one such grid. "Degree" carries Volume 4's meaning, not a probability [3]. A degree of $0.7$ on grandAdvisor(alice, carol) does not say "true in 70% of worlds," and the row of $S$ for a node does not sum to one; there is no normalization and no independence assumption anywhere. Under the Gödel reading, the degree of a derived atom is the strength of its weakest premise along its best derivation: conjunction takes a minimum, alternatives take a maximum. That reading has two consequences the chapter will cash. First, the crisp special case is a genuine special case: set every entry to exactly 0 or 1 and the algebra of minimum and maximum becomes Boolean AND and OR, so whatever the soft kernel does at degrees 0/1 must agree with a classical reasoner or the kernel is wrong. Second, degrees compose without probability's bookkeeping (no worlds, no counting), which is what lets the whole state live in two dense arrays.

The companion instantiates this state twice from the same running example, and the double instantiation is the point. The Horn face (satori_lite.py, lines 163–185) takes Volume 1's academic world: 13 nodes in Volume 3's canonical entity order, 4 labels (person, professor, researcher, student), 8 roles, and the 23 base facts of kb.py entered as hard degree 1.0. The EL face (lines 188–223) takes Volume 2's TBox after normalization, and here the reading of $S$ shifts in a way worth pausing on: the nodes are the concept names, so $S$ is a square $12 \times 12$ matrix and $S[A, B]$ is the degree of the subsumption $A \sqsubseteq B$. Its initialization is the completion algorithm's own: $S_0$ has 1.0 on the diagonal (every concept subsumes itself) and 1.0 in the ⊤ column (everything is subsumed by ⊤), and every $R_r$ starts empty, exactly the $S(A) = \lbrace A, \top \rbrace$, $R(r) = \emptyset$ start state of the EL completion oracle (el_completion.py, lines 186–188).

Both faces compile into one five-shape rule intermediate representation (IR), read off kb.RULES and the normalized TBox by shape analysis, never retyped (compile_horn, lines 131–160; el_instance, lines 196–213). Two decodings before the table. In the classical column, read $\sqcap$ as "and" between concepts, $\exists r.b$ as "has an $r$-edge to a $b$", $r \circ s$ as "$r$ followed by $s$", and $\bot$ as bottom, the concept nothing can satisfy. In the soft column, $\mathrm{softmin}_\tau$ and $\mathrm{softmax}_\tau$ are temperature-smoothed versions of minimum and maximum, defined and derived in the next section; the subscript $\tau$ is the sharpness dial carried over from Volume 3's attention, and $k$ counts the values being combined:

IR shape	classical reading	soft update fired every layer
("cr1", (A₁..A_k), B)	$A_1 \sqcap \cdots \sqcap A_k \sqsubseteq B$, or a unary Horn rule	$S[x,B] \mathrel{\oplus}= \mathrm{softmin}_\tau\big(S[x,A_1], \ldots, S[x,A_k]\big)$
("cr2", A, r, b)	$A \sqsubseteq \exists r.b$	$R_r[x,b] \mathrel{\oplus}= S[x,A]$
("cr3", r, A, B)	$\exists r.A \sqsubseteq B$	$S[x,B] \mathrel{\oplus}= \mathrm{softmax}_y\, \mathrm{softmin}\big(R_r[x,y],\, S[y,A]\big)$
("chain", r, s, t, …)	$r \circ s \sqsubseteq t$, or a two-atom Horn chain	$R_t[x,z] \mathrel{\oplus}= \mathrm{softmax}_y\, \mathrm{softmin}\big(R_r[x,y],\, R_s[y,z]\big)$
("copy", r, s)	$r \sqsubseteq s$, or a one-atom Horn rule	$R_s \mathrel{\oplus}= R_r$

The symbol $\mathrel{\oplus}=$ reads "merge into the accumulator by soft disjunction": the new contribution competes with whatever degree the cell already holds, and the softmax of the two survives. The clash rule CR⊥ needs no shape of its own; it is CR3 with $A = B = \bot$, one instance per role (line 213). The committed run reports the census: the Horn face compiles to 7 IR rules, the EL face to 19 (8 CR1, 3 CR2, 7 CR3 of which 3 are CR⊥, 1 chain), and the printout lists every Horn rule individually and reports the EL census shape by shape.

One operator, drawn once: a soft state (left) transformed by a single layer that fires all completion rules as three kinds of attention (center), unrolled to a fixed depth of three weight-tied copies whose crisp limit matches both classical oracles and whose trace is a machine-checkable proof (right). Original diagram by the authors, created with AI assistance.

One layer, three attentions

The layer needs exactly two scalar operators, and both are smoothings of Volume 4's Gödel pair. The temperature $\tau$ is a positive real number, the same sharpness dial that Volume 3's attention chapter put on the softmax [2]: small $\tau$ makes the smooth operator hug the hard one, large $\tau$ blurs it toward an average. For a list of degrees $v = (v_1, \ldots, v_k)$, with $k$ the number of values being combined (a fresh letter, since $x$ already names a node), define

$$\mathrm{softmin}_\tau(v) \;=\; -\tau \,\ln \sum_{i=1}^{k} e^{-v_i/\tau}, \qquad \mathrm{softmax}_\tau(v) \;=\; +\tau \,\ln \sum_{i=1}^{k} e^{+v_i/\tau},$$

where $\ln$ is the natural logarithm and $e^{v_i/\tau}$ the exponential function applied to a degree divided by the temperature. These are the log-sum-exp smoothings of minimum and maximum. Two facts about them do all the work, and both deserve their derivations.

Fact 1: each operator is squeezed against its hard counterpart, with a $\tau \ln k$ gap. Take softmin and write $\mu = \min_i v_i$ for the smallest entry. Every term of the sum satisfies $e^{-v_i/\tau} \le e^{-\mu/\tau}$, because $v_i \ge \mu$ and the map $t \mapsto e^{-t/\tau}$ is decreasing; and the term for the minimizer itself equals $e^{-\mu/\tau}$. Summing the $k$ terms therefore pins the sum between one copy and $k$ copies of the largest term:

$$e^{-\mu/\tau} \;\le\; \sum_{i=1}^{k} e^{-v_i/\tau} \;\le\; k\, e^{-\mu/\tau}.$$

The logarithm is increasing, so taking $\ln$ preserves both inequalities: $-\mu/\tau \le \ln \sum_i e^{-v_i/\tau} \le \ln k - \mu/\tau$. Multiplying through by $-\tau$, which is negative and so flips both inequalities, gives

$$\mu - \tau \ln k \;\le\; \mathrm{softmin}_\tau(v) \;\le\; \mu.$$

The smooth conjunction never exceeds the true minimum and undershoots it by at most $\tau \ln k$. As $\tau \to 0$ the gap $\tau \ln k$ vanishes and the squeeze forces $\mathrm{softmin}_\tau \to \min$; the mirror argument (or the duality $\mathrm{softmax}_\tau(v) = -\,\mathrm{softmin}_\tau(-v)$, which follows by substituting $-v$ into the definition and distributing the outer minus sign) gives $\max \le \mathrm{softmax}_\tau \le \max + \tau \ln k$. This is the entire meaning of "the crisp limit": every recovery claim later in the chapter is a $\tau \to 0$ statement, licensed by this squeeze.

Fact 2: the derivative of each smoothed operator is an attention distribution. Differentiate $\mathrm{softmax}_\tau$ with respect to one input $v_i$, by the chain rule through the logarithm and the exponential:

$$\frac{\partial\, \mathrm{softmax}_\tau(v)}{\partial v_i} \;=\; \tau \cdot \frac{1}{\sum_j e^{v_j/\tau}} \cdot e^{v_i/\tau} \cdot \frac{1}{\tau} \;=\; \frac{e^{v_i/\tau}}{\sum_j e^{v_j/\tau}},$$

which is exactly the normalized softmax weight vector of Volume 3, the attention distribution over the $k$ alternatives [2]; the same computation on softmin yields the attention weights of $-v/\tau$, leaning on the smallest inputs, which is how Volume 4's companion computed its conjunction gradients (fuzzy_grad.py, lines 127–134). So the pun in "symbolic attention" is not decoration. When gradients flow through this kernel, credit is distributed over premises and over rival derivations by literal attention weights; the forward pass computes a logic, and the backward pass computes attention over that logic.

The committed implementations are four lines each, numerically stabilized by the standard shift (factor $e^{-\mu/\tau}$ out of the sum so no exponent is positive), and run() asserts to $10^{-12}$ that they agree with Volume 4's scalar fuzzy_grad.softmin and satisfy the duality (satori_lite.py, lines 96–107 and 435–438):

def smin(x: np.ndarray, tau: float, axis: int = 0) -> np.ndarray:
    """softmin_τ along ``axis``:  m - τ·log Σ exp(-(x-m)/τ),  m = min."""
    m = np.min(x, axis=axis)
    return m - tau * np.log(np.sum(np.exp(-(x - np.expand_dims(m, axis)) / tau),
                                   axis=axis))

Now the layer itself. soft_layer (lines 228–258) reads only the previous state $(S^{(k-1)}, R^{(k-1)})$, fires every IR rule, and merges each contribution into an accumulator by $\oplus$; the three rule families are the three attentions of the chapter title.

Attention over premises: the conjunction body. A CR1 rule with body labels $A_1, \ldots, A_k$ scores its body at node $x$ as the softmin of the premise degrees, then merges into the head column (lines 239–241):

        if ru[0] == "cr1":      # S[x,B] ⊕= softmin_k S[x,A_k]
            c = smin(np.stack([Sp[:, li[a]] for a in ru[1]]), tau, axis=0)
            Sa[:, li[ru[2]]] = smax2(Sa[:, li[ru[2]]], c, tau)

The body is as strong as its weakest premise, softly; the temperature gates how forgiving "weakest" is. This single branch carries both faces: professor(x) → researcher(x) from Volume 1, and Volume 2's normal-form conjunctions such as the disjointness axiom Professor ⊓ Student ⊑ ⊥ [1].

Attention over rules: the ⊕-merge. Every branch ends the same way: smax2(accumulator, contribution, tau). When two different rules, or two different instantiations of one rule, derive the same head cell, their degrees compete and the soft maximum survives. This is disjunction over alternative derivations, Volume 4's Gödel t-conorm [3], and it is also precisely a softmax over the derivations of a head, attention across rules.

Attention over witnesses: the message pass. A CR3 rule $\exists r.A \sqsubseteq B$ must, for each node $x$, scan every candidate witness $y$: the conclusion at $x$ is as strong as the best $y$, and each $y$'s offer is as strong as the weaker of the edge degree $R_r[x,y]$ and the label degree $S[y,A]$ (lines 245–248):

        elif ru[0] == "cr3":    # S[x,B] ⊕= softmax_y softmin(R_r[x,y], S[y,A])
            _, r, a, bl = ru
            c = smax(smin2(Rp[r], Sp[:, li[a]][None, :], tau), tau, axis=1)
            Sa[:, li[bl]] = smax2(Sa[:, li[bl]], c, tau)

Read it as attention: the row $R_r[x, \cdot]$ is a vector of soft edge weights, the column $S[\cdot, A]$ is a vector of soft values, the softmin pairs them, and the softmax over $y$ aggregates, edge degree times source label in the Gödel currency where "times" is minimum. Role composition (chain, lines 249–255) is the same pass with a second adjacency in place of the label column, $R_t[x,z] \mathrel{\oplus}= \mathrm{softmax}_y\, \mathrm{softmin}(R_r[x,y], R_s[y,z])$: the Gödel-semiring matrix product whose crisp 0/1 case is exactly the boolean product Part IV ran on the GPU, now one branch among five. Edge emission (cr2, lines 242–244) and role inclusion (copy, lines 256–257) need no aggregation at all: a label degree flows into an edge cell, an edge matrix flows into another, each ⊕-merged like everything else.

The temperature dial, priced by the committed sweep

One committed experiment prices $\tau$ before the crisp claims arrive. Grade two base facts, advises(alice, bob) at 0.9 and advises(bob, carol) at 0.7, leave every other degree at 1.0, and read the three grandAdvisor degrees off $R$ after $L = 3$ layers (annotation_demo, lines 409–424). Gödel semantics says a derivation is exactly as strong as its weakest premise, so the true degrees are $\min(0.9, 0.7) = 0.7$ for (alice, carol), $\min(0.9, 1.0) = 0.9$ for (alice, dave), and $0.7$ for (bob, erin), whose derivation routes through bob's graded edge. The committed sweep:

[5] annotations: advises(alice,bob) graded 0.9, advises(bob,carol) 0.7; L = 3
      τ    gA(alice,carol)  gA(alice,dave)  gA(bob,erin)
  Gödel             0.7000          0.9000        0.7000   (min of premises)
   0.01            0.7110          0.9110        0.7110
   0.05            0.7540          0.9486        0.7548
   0.15            0.8406          1.0000        0.8563
   0.30            1.0000          1.0000        1.0000

At $\tau = 0.01$ the kernel sits within 0.03 of Gödel truth, asserted (lines 499–505); by $\tau = 0.30$ every degree has saturated to 1.0 and the annotation semantics is gone. The drift has two derivable sources. First, the soft $\oplus$ is not idempotent: merging a degree $v$ with itself gives $\mathrm{softmax}_\tau(v, v) = \tau \ln\!\big(e^{v/\tau} + e^{v/\tau}\big) = \tau \ln\!\big(2\,e^{v/\tau}\big) = v + \tau \ln 2$, so an atom re-derived at every layer creeps upward by up to $\tau \ln 2$ per layer, $L\,\tau \ln 2$ in total. Second, the softmax over witnesses adds phantom mass from the 12 dead candidates $y$ whose offers are 0 but whose $e^{0/\tau} = 1$ terms still enter the sum. Both effects scale with $\tau$, which is why crisp recovery is, and can only be, a $\tau \to 0$ statement.

Why lockstep is legal: monotonicity buys order-independence

The layer above fires all rules from the previous state, Jacobi-style, with no agenda, no rule ordering, and no test for convergence; the network unroll (lines 315–332) simply applies it $L$ times:

    S, R = inst["S0"].copy(), {r: M.copy() for r, M in inst["R0"].items()}
    ...
    for k in range(1, L + 1):
        S, R = soft_layer(S, R, inst, tau)

A classical reasoner earns the right to fire rules in any order from a theorem, and the theorem is Volume 1's fixpoint lesson. The immediate-consequence operator is monotone: more derived facts never disable a rule (no rule body mentions absence), so no derivation is ever retracted, and on a finite lattice a monotone, inflationary operator has a least fixpoint that every fair firing order reaches; the order changes the route, never the destination. Volume 2's completion inherits the same shape (the while changed loop of el_completion.py, lines 211–259, fires CR1 through CRχ in a fixed sweep precisely because any sweep works), and industrial EL reasoning rests on the same discipline: ELK's saturation fires completion rules to fixpoint under aggressive concurrency, correctness untouched by interleaving, which is what makes it fast [5]. The soft kernel imports the property in two pieces. Order-independence within a layer comes from the algebra: exponentiating an inner merge recovers its partial sum, $e^{\mathrm{smax}_\tau(a,b)/\tau} = e^{a/\tau} + e^{b/\tau}$, so $\mathrm{smax}_\tau\big(\mathrm{smax}_\tau(a,b),\, c\big) = \tau \ln\!\big(e^{a/\tau} + e^{b/\tau} + e^{c/\tau}\big)$: log-sum-exp is associative and commutative, and merging derivations pairwise in any order equals one joint softmax over all of them. Inflation across layers comes from merging after reading: $\mathrm{smax}_\tau(\text{old}, c) \ge \max(\text{old}, c) \ge \text{old}$ by Fact 1's lower bound, so no cell ever shrinks, and the committed run asserts exactly this at the decidedly non-crisp $\tau = 0.15$, three layers deep (lines 491–497).

That is what makes the fixed-L, weight-tied, no-halting-test stack safe to build. Because firing everything everywhere cannot overshoot (soundness is order-proof) and cannot regress (the state only grows), the only quantity at stake is how far the state has climbed toward the fixpoint, and that is governed by depth alone. Say what is given up in the same breath: a while-loop tests for convergence and always finishes the climb; a fixed stack of $L$ layers stops at $L$ waves whether or not the fixpoint has arrived, so completeness is forfeit whenever $L$ is smaller than the diameter $D$, the depth of the deepest derivation the knowledge base demands. Nothing else is forfeit. This is Part IV's truncation dial, reappearing as an architecture.

The oracle asserts: crisp recovery, twice

A capstone that only resembled its ancestors would be a diagram, not a result. The credibility test is exact: run the soft kernel at the crisp-recovery temperature $\tau = 10^{-3}$ on hard 0/1 inputs, threshold every cell at 0.5, and demand set equality with the classical oracles, imported and never reimplemented. Both asserts are committed (run(), lines 448–460):

    Sh, Rh, tr_h, sizes_h = unroll(horn, 3, TAU_CRISP, record_trace=True)
    assert atoms_of(Sh, Rh, horn) == closure and len(closure) == 47
    assert sizes_h == tp_sizes, "wave profile differs from T_P's"
    Se, Re, tr_e, _ = unroll(el, 3, TAU_CRISP, record_trace=True)
    assert atoms_of(Se, Re, el) == el_closure and len(el_closure) == 46

The first oracle is Volume 1's forward chainer: least_fixpoint iterates the immediate-consequence operator $T_P$ until nothing changes (forward_chain.py, lines 52–63), and on the academic world it closes 23 base facts to 47 atoms, two waves of new derivations and a third that confirms the fixpoint. The kernel's thresholded state equals that closure exactly, and more: its per-layer atom counts reproduce $T_P$'s wave profile 23 → 41 → 47 → 47 step for step, 18 new atoms in wave one, 6 in wave two, none in wave three. The second oracle is Volume 2's EL completion. The kernel's saturated state equals the oracle's saturated $S$ and $R$ (46 atoms), and the harness then goes one step further in fairness: it hands the kernel's own thresholded state to the oracle's own report generators, elc.subsumptions and elc.unsatisfiable, and asserts the classification matches, 8 subsumptions between named concepts and the 2 unsatisfiable concepts TenuredStudent and TenuredStudentAdvisor (lines 454–460). The committed printout, whose label "the C8 dry run" reads ahead: C8 is the number the SATORI claims matrix assigns to its crisp-soundness claim, and the claims chapter grades it in full:

[2] crisp recovery at L = 3 (the C8 dry run) — exact, both oracles
  Horn: 47 atoms == the forward-chain closure; wave profile 23→41→47→47 == T_P's
  EL  : 46 atoms == el_completion's saturated S/R; 8 subsumptions,
        unsatisfiable = ['TenuredStudent', 'TenuredStudentAdvisor']

Why insist on both oracles? Because they exercise different rule shapes. The Horn face is all individuals and binary structure: chains, a transitive closure that feeds its own body, a diagonal-masked colleague rule; it never touches CR2, CR3, or ⊥. The EL face is all concept names and existential structure: edge emission from axioms $A \sqsubseteq \exists r.B$, message passes for $\exists r.A \sqsubseteq B$, and the clash rule that propagates unsatisfiability backward along roles; its deepest derivation is exactly the kind the Horn face lacks. A kernel that recovers one face might still botch the other. Recovering both, from one layer and one IR, is the evidence that the fusion is an operator and not two operators in a trench coat.

The truncation law, re-run in attention clothing

Part IV measured what a fixed depth budget costs a reasoner; here the same law re-emerges from inside the network. For every $L$ from 0 to 4 the harness unrolls the stack, reads the atoms, and checks two things: soundness, the atom set is a subset of the true closure at every depth, and recall, the fraction of derivable-but-not-given atoms actually derived (lines 462–476). The committed table:

[3] the truncation law — sound at every L, complete iff L ≥ D = 3
      L   Horn atoms  recall    EL atoms  recall
      0           23   0.000         23   0.000
      1           41   0.750         32   0.391
      2           47   1.000         41   0.783
      3           47   1.000         46   1.000   ← D = 3: joint task complete
      4           47   1.000         46   1.000
  (the Horn face saturates at L = 2; the EL clash ⊥ ∈ S(TenuredStudentAdvisor)
   needs the third wave — truncation only ever loses recall, never soundness)

Read the two columns against each other. The Horn face saturates at $L = 2$: its longest derivation is citesTransitively(p3, p1), one copy step plus one chain step. The EL face needs $L = 3$: the clash ⊥ ∈ S(TenuredStudentAdvisor) is a three-wave derivation (wave one lands Professor and Student in S(TenuredStudent) and emits the advises edge from TenuredStudentAdvisor; wave two fires the disjointness conjunction Professor ⊓ Student ⊑ ⊥ at the edge's target; wave three is CR⊥ carrying ⊥ back across the edge), so the joint task is complete exactly at $L = 3$, the academic world's derivation diameter, and stays complete at $L = 4$ because a fixpoint, once reached, is fixed. The asserts are sharper than the table: recall is monotone in $L$ for both faces, the Horn face hits 1.000 at 2 while the EL face is asserted still short of 1.000 (0.783 in the table), and depth 3 closes both (lines 473–476).

One discipline from earlier in the volume must be restated here, because Part VII's claims chapter will lean on it. This kernel's errors run in exactly one direction: at $L \lt D$ it misses derivable facts and never asserts an underivable one, sound but incomplete, precision 1.0 with recall priced by the table. Volumes 3 and 4's query embeddings ran the opposite direction: geometry generalizes, so a box or a beta distribution happily scores atoms the knowledge base does not entail, complete-ish but unsound, recall bought with precision. A production system stacking both (this kernel as substrate, learned embeddings above it) inherits both error directions at once, and a calibration story that does not track which direction each component errs in cannot be honest. That is a promissory note this chapter issues and SATORI's claims chapter must pay.

The trace is a first-class output, not a rationalization

Part I of this volume drew a hard line between an explanation extracted from a decision procedure and an explanation reconstructed about one: justifications were certified by theorem, and faithfulness had to be checked by deletion experiments precisely because post-hoc stories float free of the mechanism. Symbolic attention makes the Part I lesson architectural: the kernel records its attention as it reasons, and the record is the proof. At the crisp limit, every atom first derived at layer $k$ gets a trace entry $(k, \text{rule}, \text{parents})$, where the parents are the argmax of the derivation that fired; since at $\tau \to 0$ all crisp derivations tie at degree 1, the deterministic tie-break (fixed rule order, then sorted atoms) is the argmax (crisp_step, lines 261–301). The trace is then consumed by the toughest reader available, a proof checker: check_proof (lines 337–371) re-derives every recorded atom, asserting that its rule is in the rule set, that the parents instantiate that rule's shape under a consistent variable binding, that guards hold, and that every premise was derived strictly earlier. All 47 derived atoms across both faces pass, asserted (lines 478–489), and the committed run prints the derivation this series has been deriving since Volume 1:

[4] attention trace → machine-checked proofs (all 24 + 23 = 47 derived atoms pass)
  grandAdvisor(alice, carol)   [layer 1, CRχ: advises(x,y) ∧ advises(y,z) → grandAdvisor(x,z)]
      advises(alice, bob)   [base fact]
      advises(bob, carol)   [base fact]
  citesTransitively(p3, p1)   [layer 2, CRχ: cites(x,y) ∧ citesTransitively(y,z) → citesTransitively(x,z)]
      cites(p3, p2)   [base fact]
      citesTransitively(p2, p1)   [layer 1, copy: cites(x,y) → citesTransitively(x,y)]
          cites(p2, p1)   [base fact]
  proof depths: grandAdvisor(alice, carol) = 1, citesTransitively(p3, p1) = 2

Notice what kind of object this is. The Part VII artifact (an attention record) is being verified by the Part I machinery (a rule-instantiation checker), and the verification is not a similarity score but a binary pass over every step. Contrast the two explanation regimes this volume has met. A post-hoc attribution on a black-box model asks "which inputs, if perturbed, change the answer?" and can be unfaithful without anyone noticing. This trace cannot be unfaithful in that sense, because it is not testimony about the computation; it is the computation, written down as it happened, in a language (rule instantiations) that admits a checker. The design cost was paid upstream: the kernel's state had to be made of symbols with fixed meanings (label columns, role matrices) for "argmax parents" to even be a well-typed thing to record. That cost is the entire subject of Part II: a learned model whose internal symbols drift loses exactly this property, which is why reasoning shortcuts and identifiability sit between this chapter and any claim that a trained SATORI inherits the guarantee.

A single burst, honestly

The source project's name commits it to a metaphor. SATORI is the Zen term for sudden awakening, and the project's own gloss contrasts 돈오 (sudden enlightenment) with 점수 (gradual cultivation): reasoning as one burst of salience rather than the slow, goal-by-goal crawl of backward-chaining proof search, the mode of computation the differentiable-proving lineage inherited [4]. This chapter has now built enough to state what the metaphor is worth, and Part IV already fixed the exchange rate. The completion core of the OWL 2 EL and RL profiles is PTIME-complete (complete for polynomial time), and Work-Depth Trade-offs stated the consequence precisely: its fixpoint admits no constant-depth or polylog-depth evaluation at polynomial total work, that is, no evaluation in NC (the class of problems solvable in polylogarithmic depth with polynomially many processors), unless NC and the polynomial-time class P coincide, which is not believed; the proof is far beyond this volume, and the companion demonstrates the behavior, not the theorem, in its truncation table. So on the core, "a single burst" cannot mean zero-depth insight. What it honestly means is bounded-depth salience: all the parallelism that does exist is spent, every rule fires everywhere at every layer with no agenda and no goal stack, and the serial residue is compressed into $L$ lockstep waves whose count is chosen ahead of time and whose recall is priced, per depth, by the committed table. Zero-depth reasoning exists, but only where the theory grants it: the first-order-rewritable fragments that Materialization versus Rewriting ran through a constant-depth query rewrite, a lane this kernel deliberately does not occupy. The dual-process romance, a slow deliberate System 2 collapsed into a flashbulb System 1, survives in corrected form: the flash is real, it is just $L$ frames long, and the honest engineer publishes $L$, publishes $D$, and publishes the recall curve between them.

The unsolved part

Two deliberate absences separate this kernel from the system it prefigures, and both are the next chapter's opening problems. First, the kernel's "soft unification" is degree-gating over existing symbols: a rule for advises can fire only on the advises matrix, at whatever degree its cells hold. It cannot notice that supervises, a symbol it has never been given a rule for, behaves almost identically and deserves the same inferences. Matching merely similar symbols is the genuinely neural half of the fusion, the line running from Volume 3's soft unification through Volume 4's differentiable provers [4], and it is deliberately outside this chapter's kernel because it requires an embedding substrate: symbols must live in a geometry before similarity between them is even defined. That substrate, and the precision risk it reintroduces, enters with the architecture chapter. Second, $\tau$ is a single global dial here, frozen for the whole stack, and the committed sweep showed the dial is a semantics knob: 0.01 preserves Gödel truth to within 0.03, 0.30 destroys it entirely. A production kernel wants learned, per-rule temperatures, sharp where a rule's body must be strict, soft where gradient flow through a long derivation matters more than exactness. Whether per-rule temperatures can be learned without the optimizer discovering that "blur everything to 1.0" is a loss-minimizing reasoning shortcut is exactly the kind of identifiability question Part II taught this volume to ask, and it is open.

Why it matters

For the series, this chapter is the arrival the preface promised: the point where the symbolic and neural halves stop being chapters in different volumes and become one object with two readings. Every load-bearing part was built earlier and is reused, not reinvented: the fixpoint theory of Volume 1 licenses the lockstep stack, the completion calculus of Volume 2 supplies the rules, the attention algebra of Volume 3 supplies the operators and the temperature, the Gödel semantics of Volume 4 makes the operators a logic, and the trust instruments of Parts I through IV of this volume are what the kernel is then held to: oracle equality, per-depth soundness, checkable traces, an honest depth price. For the reader's own research, the chapter is a worked template for a claim style that the frontier increasingly demands. The interesting statement is almost never "we fused X and Y"; it is the ledger underneath: which classical guarantee survives the fusion (soundness, here), which is spent and metered (completeness, by the recall table), which artifact certifies the survivors (asserts against oracles, a proof checker on the trace), and which knob would break the semantics if learned carelessly ($\tau$). A fusion paper that fills in that ledger is research; one that does not is a diagram.

Key terms

• Symbolic attention: the rendering of a completion procedure as an attention operator: rule bodies scored by softmin over premises, rival derivations merged by softmax, role composition as a message pass over soft adjacencies, on a state of Gödel degrees.
• Soft label matrix $S$ / soft adjacency $R_r$: the reasoner's entire state; $S[x, A]$ is the degree to which label $A$ holds of node $x$ (on the TBox face, the degree of the subsumption $A \sqsubseteq B$), and $R_r[x, y]$ the degree of the edge $r(x, y)$.
• Gödel degree: a truth value in $[0,1]$ combined by minimum (conjunction) and maximum (disjunction); not a probability, and carrying no independence or normalization assumptions.
• softmin$_\tau$ / softmax$_\tau$: the log-sum-exp smoothings of min and max, squeezed within $\tau \ln k$ of their hard counterparts and converging to them as $\tau \to 0$; their derivatives are attention distributions.
• Temperature $\tau$: the sharpness dial shared with Volume 3's attention; near 0 the kernel is a classical reasoner, and the committed sweep shows annotation semantics washing out as $\tau$ grows.
• Lockstep (Jacobi) firing: every rule fires from the previous state simultaneously, with no schedule; legal because the completion operator is monotone and inflationary, so firing order cannot change the fixpoint.
• Fixed-$L$ weight-tied unroll: the same layer applied $L$ times with no halting test; sound at every $L$, complete exactly when $L \ge D$.
• Derivation diameter $D$: the depth of the deepest derivation the knowledge base requires; $D = 3$ for the joint academic-world task, set by the EL clash derivation.
• Attention trace: the per-atom record (layer, rule, argmax parents) written during the forward pass; machine-checked here into a proof, the faithfulness-by-construction property.
• Crisp recovery: the $\tau \to 0$ statement that the thresholded soft state equals the classical closure; asserted as set equality against both the Volume 1 and Volume 2 oracles.

Where this leads

This chapter froze every weight at 1: the rules were given, the router had nothing to choose, and the only neural artifact was the smoothing itself. The SATORI Architecture unfreezes the design: an embedding substrate under the symbols so that soft unification can match what was never syntactically identical, a learned router deciding which rules deserve attention, per-role sparse adjacencies and locality shards so the state survives real ontologies, and the four claimed properties (learnable routing, faithful traces, parallel scale, calibrated confidence) hung on the one operator this chapter built and audited. The kernel stays; everything around it becomes trainable, and every trust instrument in this volume comes along to check what training does to the guarantees.

---

Companion code: examples/frontier/satori_lite.py implements the soft Gödel operators, the five-shape rule IR, the lockstep layer, the fixed-$L$ unroll, the trace recorder, and the proof checker, importing Volume 1's forward_chain.py and Volume 2's el_completion.py as its oracles and Volume 4's fuzzy_grad.py as its scalar cross-check. Run python3 examples/frontier/satori_lite.py to reproduce every number in this chapter; the run is deterministic, and every claim, both oracle equalities, soundness at every depth, all 47 proof checks, and the annotation sweep, is guarded by an assert.