The Honest Verdict: The State of Neuro-Symbolic AI

📍 Where we are: Part IX · The Verdict — Chapter 23. Doing the Next Research turned the gap map into first experiments a single researcher can start on Monday; this final chapter reads the whole five-volume ledger aloud, marks every line settled or open, and names the committed check that keeps each line honest.

Every volume of this series ended in a verdict, and every verdict had the same form: not a ranking, not a manifesto, but a ledger whose lines are claims and whose collateral is running code. This chapter is the series-level instance of that form, on the state of neuro-symbolic AI as this series can honestly attest to it: the field whose integration patterns a well-known taxonomy organized into a common vocabulary [1], and whose case for a "third wave" of AI, systems that both learn and reason, the verdict below finally weighs with receipts rather than enthusiasm [2]. What makes this ledger different from the three before it is scope: its lines cite chapters, and every line names the committed check, in one of five runnable companion suites, that a reader can execute today to test whether the line is still true. The verdict, in other words, is not what this chapter says. It is what happens when you run the code.

The simple version

Imagine the final inspection of a building that took five construction phases. A bad inspection is a speech: the architect walks you through and says trust me. A good inspection is a wall of switches: every subsystem installed over the five phases was left with its own test switch, and the report is just the record of flipping every one and watching every light. This chapter is that wall of switches for a five-volume series. Eighty switches, five panels, one afternoon to flip them all. Settled is what lights up green when you press it; open is honestly labelled "no switch installed yet"; and the report ends not with applause but with the toolbox handed to you.

What this chapter covers

• The ledger's form, one last time: the verdict chapters of Volumes 2, 3, and 4 compressed to a sentence each, and the series-level twist: five harness summary lines quoted as the heartbeat behind every claim below.
• Settled, in four parts: exactness is programmable, gradients flow through logic at a known price, depth has physics, and trust has instruments, each part a list of committed numbers with the module that re-derives them, and "settled" meaning: at the scales and fragments stated, with the systems literature carrying the rest.
• Open, without flinching: the eight gaps in one line each with their instrument-readiness, the interaction matrix as the nearest tractable frontier, and the scale asterisk written out in full.
• The mutual debt: the series' closing argument, symbols owe learning their structure and vectors owe reasoning their guarantees, defended against both purisms using only receipts already on the table.
• The method as the verdict: four imperatives (oracle first, claims as experiments, instruments beside models, ledgers in public), and the honest naming of the series' final artifact.

The ledger, one last time

Three verdicts precede this one, and each fits in a sentence. Volume 2 found that symbols buy correctness you can trust and explain, on knowledge you must write down and keep consistent. Volume 3 found the mirror image: geometry buys plausibility you can train, on knowledge nobody wrote down, at the price of certainty you can no longer have. Volume 4 refused to crown either and instead priced every crossing between them, a ledger of buys, costs, and guards in which "is fuzzy better than probabilistic?" was retired in favor of "what does each pay, and which committed check guards the claim?". That progression is itself a walk through the field's design space, the one the survey literature maps along semantics, inference placement, and learning target [3]; the series simply walked it with a harness in hand.

The series-level ledger below adds the discipline that makes it auditable: every line cites the chapter that taught it, and behind every chapter stands one of five acceptance harnesses whose exit code is the verdict on everything that chapter asserted. Their summary lines are the series' heartbeat, quoted exactly as the committed runs print them (examples/logic/README.md line 34, examples/symbolic/README.md line 39, examples/neural/README.md line 51, examples/integration/README.md line 62, examples/frontier/README.md line 67):

logic companion: 12/12 competency checks passed
symbolic companion: 13/13 competency checks passed
neural companion: 15/15 competency checks passed  (16s)
integration companion: 21/21 competency checks passed  (19s)
frontier companion: 19/19 competency checks passed  (56s)

Eighty checks, five suites, one running example threaded through all of them: the thirteen-entity academic world that Volume 1 introduced and no volume ever abandoned. Everything called settled below is settled in this sense: a claim, an instrument, and a green light you can re-derive. Everything called open is open in the same sense: no instrument yet exists, and this chapter says so plainly.

The series' last ledger: four settled rows on the left, each wired to the harness heartbeat that keeps it true; eight open gaps and their interaction arrows on the right; the scale asterisk under everything; and the toolbox changing hands. Original diagram by the authors, created with AI assistance.

Settled, part one: exactness is programmable

The first settled line is the series' oldest: a reasoning procedure can be written down, run to completion, and checked for exact agreement with an independent implementation, and this survives every change of machinery underneath. Volume 1's forward chainer closed the running example's Horn knowledge base to its least fixpoint in three waves, 47 atoms with 24 derived, and its backward prover agreed on every membership query. Volume 2's EL completion classified the 14-axiom academic ontology, 8 nontrivial subsumptions and 2 unsatisfiable concepts, and matched HermiT, an independent tableau reasoner built on entirely different principles. This volume rebuilt the same fixpoint twice more under hostile conditions and demanded the same equality: GPU Reasoning vectorized the completion into boolean matrix algebra and matched the Volume 2 oracle cell for cell while closing 100 TBox (terminological box, the ontology's axiom set) variants in one stacked tensor pass, and Materialization vs. Rewriting answered the same queries three ways, materialized lookup over 47 stored facts, rewriting over 23, and the SLD (selective linear definite resolution) oracle, with three-way agreement throughout and DRed (delete-and-rederive) deletion maintenance overdeleting exactly 2 facts and re-deriving exactly 1. Four implementations, three volumes, one answer set: exactness is not a property of one program but a contract any number of programs can be held to.

What "settled" responsibly means: at the scales and fragments stated. These receipts concern Horn rules and the EL family on a desk-sized world; they do not certify OWL (Web Ontology Language) DL at hospital scale or Datalog over billions of triples. Those regimes are real, and their evidence lives in the systems literature this series cited rather than reproduced: the ELK and CEL line of EL-profile reasoners, the Konclude and HermiT line of expressive-DL reasoners, the RDFox line of parallel materialization, the LUBM, OWL2Bench, and ORE benchmark tradition. The settled claim is precise: the semantics is fragment-dependent but the discipline is not, and every scale-up in that literature is checkable against the same kind of oracle this series carried in its pocket.

Settled, part two: gradients flow through logic, price known

The second settled line is Volume 4's, and its ledger of 21 checks compresses to three headline receipts with the price column kept visible. First, the disjoint-sum repair, the receipt that semantics is chosen, not assumed: summing the running example's two grandAdvisor proof probabilities as if they were exclusive gives $0.81 + 0.765 = 1.5750$, not a probability at all, while inclusion-exclusion subtracts the doubly counted shared-fact conjunction, $0.81 + 0.765 - 0.6885 = 0.8865$, confirmed by enumerating all $2{,}048$ possible worlds (Distribution Semantics derives every step). Second, the gradient semiring of DeepProbLog, the receipt that learning can ride exact inference rather than replace it: one upward pass over a compiled circuit returns the query probability together with every partial derivative, and the hand-derived gradients answer to two independent oracles, central finite differences (committed maximum discrepancy $2.7 \times 10^{-13}$) and a full autograd re-implementation agreeing to the $10^{-6}$ tolerance across three derivative pipelines. Third, the training-free surprise of Fuzzy and Training-Free CLQA: composing a pretrained one-hop predictor through fuzzy conjunctions and disjunctions answered five multi-hop query types far above graph traversal with no end-to-end training at all, never missing an easy answer, with a proof checkable edge by edge.

The price column keeps this line honest. Truncation: the top-$k$ escape from exact counting (keeping only the $k$ highest-probability proofs and discarding the rest) is a lower bound that climbs toward the truth ($0.765 \to 0.934$ on the committed exhibit) but never certifies its own distance from it. Calibration debt: not one confidence Volume 4 produced meant its number. Concept risk: a model can satisfy every query-level target while its internal symbols mean the wrong things, the debt this volume named reasoning shortcuts and learned to count. Gradients through logic are settled the way a mortgage is settled at signing: the terms are known, and the payments are real.

Settled, part three: depth has physics

The third settled line is the one this volume added, and it is the series' most portable lesson: parallelism, depth, and exactness form a budget, not a wish list. Four results assemble it. First, the work-depth ledger of Work-Depth Tradeoffs, counted operation by operation: closing a 512-node relation chain takes the semi-naive engine 510 sequential waves at $261{,}121$ elementary operations, while repeated boolean matrix squaring closes it in $9{+}1$ parallel steps at $2{,}681{,}733{,}120$ operations, a measured $10{,}270\times$ work premium for a roughly $50\times$ depth saving. You may buy shallow; you pay in work.

Second, the ceiling. The theorem behind it, stated precisely and not proved here: every transformer whose forward pass carries $O(\log n)$ bits of numeric precision, where $n$ is the input length and $O(\log n)$ means the bit budget grows only logarithmically with it, can be simulated by a logspace-uniform TC⁰ circuit family, that is, by constant-depth, polynomial-size circuits of threshold gates (gates that fire when a weighted sum of their inputs crosses a threshold), with uniform meaning a single logarithmic-space algorithm writes down the circuit for each input length [4]. The consequence is a genuine ceiling: any problem provably outside TC⁰, and iterated composition in the permutation group $S_5$ (the 120 shufflings of five objects) is complete for the presumably larger class NC¹ (the problems solvable by logarithmic-depth circuits) by Barrington's theorem, cannot be computed at all input lengths by such a transformer unless the two classes collapse, which complexity theory does not expect. (The companion's own iterated-$S_3$ task stays inside TC⁰; the depth-ceiling chapter uses it as a mechanism testbed, not a separation witness.) The proof is beyond this volume. What the companion demonstrates instead is the behavioral shadow of that physics: The Transformer Depth Ceiling trained a ladder of fixed-depth networks and watched parity generalization cliff at input lengths 3/6/6 for depths 1/2/3, with beyond-cliff accuracy at chance, 0.506/0.500/0.500 against the 0.500 chance line, while a depth-scaled control kept tracking. A cliff in a toy MLP (multilayer perceptron) is evidence of the mechanism, never a proof of the theorem.

Third, the exchange rate. Chain-of-Thought showed the ceiling is rentable: the same fixed-depth model that cliffs at length 5 (tail accuracy 0.159) stays exact, minimum accuracy 1.000, out to 32 steps when it may emit intermediate results and re-read them, buying back one layer of lost depth per emitted step. Fourth, the contract that makes rented depth trustworthy: Reinforcement and Verifiers gated a proposal policy behind a proof checker, cutting wrong derivations from a rate of $0.247$ to exactly $0$ at recall $0.979$, then used the same verifier as a reward to lift the policy's exact-proof rate from $0.205$ to $0.535$. Soundness bought for recall, at a price the curve states. Four results, one lesson, portable to any architecture the reader will ever evaluate: ask what the depth budget is, who pays the work bill, and which side of the exactness line the residual error falls on.

Settled, part four: trust has instruments

The fourth settled line is this volume's center of gravity, and it earns Part IX its place in one sentence: a claim without an instrument is now a choice, not a necessity. Five failure modes of trustworthy reasoning each received a measuring device, validated on a case where it must fire and a case where it must not, with its numbers committed to a harness that re-derives them on every run.

instrument	the question it answers	the committed separation	module
justification enumeration	which axioms carry this entailment?	7 MinAs (minimal axiom sets) over 4 entailments, equal to the $2^{14} = 16{,}384$-subset brute force	justifications.py
erasure faithfulness	is the offered explanation the actual reason?	comprehensiveness: occlusion 0.3659, attention 0.2497, random 0.0789, on one 0.9609-accurate model	faithfulness.py
shortcut counting	are the concepts right, or only the labels?	label accuracy AccY 1.000 = 1.000 while concept accuracy AccC splits 0.750 vs 1.000	rsbench_lite.py
calibration (ECE, expected calibration error)	do the confidences mean their numbers?	ECE 0.0245 → 0.0167 at the fitted temperature $\tau^* = 1.4172$; accuracy 0.9683 and AUC (area under the ROC curve) 0.9136 bit-identical	calibration.py
abstention curves	can the system decline instead of guessing?	structural (translate-prove) coverage 0.9293 at zero wrong answers	abstention.py

Read the rows in order. Justifications enumerate: each MinA (minimal axiom set) is a minimal subset of the ontology that still entails the result, Reiter's hitting-set tree matched the exhaustive search over all 16,384 axiom subsets, and every computed repair provably killed its entailment. Faithfulness has erasure: a deliberately unfaithful attention pattern on a right-answering classifier was caught because deleting what it pointed at barely moved the prediction. Shortcuts have counters, and the imported theory deserves a precise statement: for a task whose label is a known Boolean function of $k$ latent concepts (here $k$ counts the concept bits), the deterministic optima of the label-only training objective are exactly the concept maps whose composition with the task function reproduces every training label, and the number of such optima, written $N_{\text{opt}}$, has a closed form counted over the distinct inputs the training distribution supports [5]. The derivation is beyond this volume. What the companion demonstrates instead is the count itself: exhaustive enumeration reproduces the closed forms exactly, $16/32/64$ optima for XOR (exclusive or) over $k=2$ concepts as the support shrinks and $65{,}536 \to 1{,}048{,}576$ for $k=3$, and then exhibits the predicted phenomenon, a model with perfect label accuracy, concept accuracy 0.750, and concept-level ECE 0.2467, repaired to 1.000 and 0.0013 by supervising just 10 percent of concepts. Calibration has ECE, repaired by one scalar: a single held-out temperature (the $\tau^*$ of the table) cut both calibration error and negative log-likelihood while touching no accuracy-flavored number, because dividing scores by a positive constant reorders nothing. And abstention has curves: three policies in one table, Chow's rule on the calibrated confidence (coverage 0.9841, silent-wrong rate 0.0159), the open-world interval reading that refuses the unknown zone (coverage 0.8651), and the structural translate-then-prove policy whose zero wrong answers hold by construction because its answers are proofs.

The volume then bound all five instruments into one regression discipline: suite_harness.py re-runs every instrument from scratch under one seeded protocol and asserts each of the 26 committed headline numbers equal, digit for digit, to the value frozen in the file (lines 133–143):

def _regress(instrument: str, derived: dict[str, str]) -> None:
    """The regression gate for one instrument: every re-derived headline
    string must equal its committed value exactly.  Committed and derived
    must also cover the SAME keys, so a silently dropped check fails too."""
    want = COMMITTED[instrument]
    assert set(derived) == set(want), \
        f"{instrument}: check set drifted ({set(derived) ^ set(want)})"
    for key, got in derived.items():
        assert got == want[key], \
            f"{instrument} regression: {key!r} committed {want[key]!r}, " \
            f"re-derived {got!r}"

The committed run ends with the suite's one-line verdict, five separations that plain accuracy cannot see, each cleared by an asserted margin (suite_harness.py lines 444–450):

SUMMARY suite_harness: checks=26/26 accC_gap=+0.250 ece_gap=-0.0078 comp_gap=+0.1162 cliff_gap=+3 cons_gap=+0.5141 checklist=4y/3n

The final field is the honesty clause: the harness scores its own mini-suite against the design principles of the real benchmark generation, rsbench, LogiCity, KANDY, and concedes three properties a desk cannot have, with an assert that fails if the checklist ever stops conceding anything (suite_harness.py lines 369–372). Instruments that cannot indict themselves are marketing.

Open, without flinching

The gaps chapter mapped eight open problems; the verdict recalls each in one line with its instrument-readiness, because an open problem with a ready instrument is a different object from one without. G1, the exact/learnable split: instrumented at toy scale (the planted-rule protocol recovers a hidden rule with router mass 0.9718; the crisp limit recovers both classical oracles), unsolved at vocabulary scale. G2, rule-search explosion: dodged here (25 templates), uninstrumented where it bites, at thousands of relations. G3, CPU-bound symbolic inference: a proxy instrument exists (the stacked tensor pass, wall-clock labelled as asserted nowhere), while the queries-per-second comparison against PyReason and Scallop-class engines remains cited-only. G4, ontology-blind rule learning: the ablation is degenerate on a kernel built from the TBox, so the geometric evidence stays with the Box2EL and TransBox line. G5, non-transferability: partially instrumented, Volume 4's structural scorer transferred zero-shot to a second toy world (a mean reciprocal rank, MRR, of 0.83 against random 0.22), but a second ontology is still missing. G6, explanation faithfulness: the best-instrumented gap in the series, erasure plus MinA-containment, comprehensiveness 8/8 and sufficiency 4/4 on the capstone. G7, uncertainty, calibration, and shortcuts: instrumented end to end, ECE, counters, intervention probes. G8, meta-cognition: instrumented as abstention, coverage against risk, with the open-world interval making "I don't know" a value in the data model rather than a failure of nerve.

The nearest unexplored ground is not any single gap but their interactions, three of which the capstone named as experiments waiting for a desk: routing versus traces (does a learned router still produce traces containing a true minimal justification?), batching versus intervals (does the stacked fixpoint preserve open-world annotations, or does vectorization quietly close the world?), and training versus calibration (does end-to-end fine-tuning destroy the calibration a frozen kernel posts?). Each pairs two instruments this volume already built; the experiment is composition, not invention.

And then the asterisk, written out in full because it stands on every settled line above. Every committed number in five volumes was measured on a desk: thirteen entities, 47 atoms, 46 subsumptions, an embedding model of dimension $d = 16$, classifiers of a few thousand parameters, probes of a few hundred points. The datacenter claims, billions of triples materialized, ontologies with hundreds of thousands of concepts classified in seconds, ceilings measured on real language models, ride on citations, and citations can rot: results get corrected, benchmarks saturate, code links die. The reader's audit duty follows: where this series committed a number, run the harness; where it cited one, treat the citation as a claim with a decaying half-life, and before building on it, find the artifact and press its switch.

The mutual debt

The series' closing argument is a sentence shaped like a theorem, and by now every clause of it has receipts. Symbols without learning cannot meet the world's width. This is the unwritten-edge lesson that opened Volume 3, and the running example's own history: hand-written rules gave way to a trained geometry ranking the never-written edge near the top (filtered MRR 0.7778, the ranking scored with known true edges removed, against a frozen-random 0.1062, where the exact traversal scores 0 on every hard answer by definition), and then to routed rules, a softmax over templates recovering the hidden grandAdvisor rule exactly from its answers alone. The knowledge base anyone can afford to write is always a strict subset of the knowledge their queries need; only learning crosses that gap. Learning without symbols cannot keep its promises. This is the soundness lesson of every probe since Volume 3: the region geometry that carries logic exactly only when constructed, the 98.96-percent-accurate soft reasoner that is 48.6 percent consistent under paraphrase while the translate-then-prove pipeline holds 100 on every parsed probe, the calibrated confidence that still needed a verifier gate before its answers could be promised rather than predicted. And the third clause, the architectures that matter are exactly those that let each pillar hold the other to account, is not a hope; it is the capstone's committed table, printed by satori_eval.py (lines 625–651):

[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

Read that table as the field in miniature and both purisms fall to receipts already on the table. To the symbolic purist: your exact traversal scores 0 on every answer nobody wrote down, an MRR of 0.1488 beneath even the 0.230 chance floor, while the neural half of the same operator reaches 0.568 with its soundness anchor intact. To the connectionist purist: every neural number in that table is trustworthy only because a symbolic instrument stands beside it, the MinA behind the trace, the interval behind the abstention, the crisp limit behind the kernel. The integration taxonomy gave these compositions their names [1]; the third-wave argument said systems must both learn and reason [2]; the surveys mapped the design space between them [3]. What the series adds is the audit: a five-volume demonstration that the space can be walked with an oracle in one hand and an instrument in the other, and that the architectures which survive the walk are the mutually accountable ones.

The last page: the method is the verdict

Strip away every particular number above and what remains is a method, restated as the four imperatives the series has practiced since its first chapter. Oracle first: build the exact version of the task, however small, before anything learned, and keep it runnable beside every experiment; every soundness claim in five volumes reduces to an equality against an oracle someone bothered to write. Claims as experiments: state what a system is supposed to do as a matrix of checkable claims before measuring it, and let the matrix say verified with this number or cited-only, and why. Instruments beside models: for every asserted property, an independent, fail-capable measuring device; count a paper's advertised properties, count its instruments, and read the difference as pitch. Ledgers in public: commit the numbers, seed the randomness, make the harness's exit code the verdict, so that "still true" is a command anyone can run rather than a reputation anyone must trust.

The state of neuro-symbolic AI, as this series can honestly attest to it, is that this discipline is now possible end to end: from a Horn closure to an EL oracle to a trained geometry to a differentiable prover to a calibrated, abstaining, trace-faithful kernel, with an instrument at every joint and a green light behind every claim. That fixes what the series' final artifact actually is. Not a conclusion; conclusions are sentences, and sentences cannot be re-run. A reader: one who now owns four working engines, five instrument kits, an honest map of eight gaps with three marked interactions, and a Monday plan, and who has personally executed every step of the method the field's next results will be held to.

The unsolved part

The verdict's own method carries an open question the verdict cannot close: whether the discipline survives the loss of its oracles. Every equality assert in eighty checks compares a system against ground truth that exists only because the world is small, a $2^{14}$-subset brute force, an exhaustively enumerable optima space, a fixpoint a second implementation can reproduce overnight. At the scales where the field's real claims live, the oracle is gone: no brute force enumerates the justifications of a hundred-thousand-concept ontology, and no exact count certifies the shortcut census of a perception model. The suite's own checklist concedes exactly this, printing the row [ no] public scale: big OOD splits, (eps,delta)-guaranteed counting. What replaces oracle-equality when no oracle fits in memory is genuinely unsettled: statistical certificates with explicit failure probability, interval bounds that degrade gracefully, verifier gates that certify individual answers rather than whole systems. Each candidate exists in fragments; none yet composes into the end-to-end ledger this series ran at desk scale. The last open problem the series records is about itself: scaling the method is as unsolved as scaling the systems it measures.

Why it matters

This chapter is the series' claim about what its five volumes were for. Not a tour, an apprenticeship: Volume 1 taught the reader to build oracles, Volume 2 to demand soundness and completeness by name, Volume 3 to measure what geometry holds and confess what it cannot, Volume 4 to price every gradient that crosses a logical boundary, and Volume 5 to instrument trust, count depth, and put a claims matrix where a pitch would have gone. The portable asset is the reflex: when the next architecture arrives, and it will arrive advertised, the questions are already loaded. Where is the oracle? Which claims are experiments? Which instrument fails if the property is fake? Where is the ledger, and does it still run? A field matures not when its systems stop being wrong but when its wrongness becomes measurable, attributable, and priced. The evidence of five volumes is that neuro-symbolic AI has crossed that line at desk scale, and that crossing it at every other scale is now an engineering agenda with named gaps rather than a philosophical dispute with named camps.

Key terms

• Ledger: the verdict form this series uses in place of rankings: lines are claims, columns are buys, costs, and guards, and every line names the committed check that keeps it true.
• Committed check: an assert in a runnable harness whose expected value is frozen in the repository, so a re-run either reproduces the claim digit for digit or fails loudly.
• Oracle-equality: the strongest settled-claim standard available at desk scale: exact agreement between a system and an independent exact implementation.
• Instrument: an independent, fail-capable measuring device paired with a claim, validated on a case where it must fire and a case where it must not; the unit of trust in this volume.
• Heartbeat: the five suite summary lines (12/12, 13/13, 15/15, 21/21, 19/19) whose joint green status means every committed number in the series still reproduces.
• Scale asterisk: the standing qualifier on every settled line: measured on a desk, with datacenter-scale evidence carried by citations the reader must treat as decaying claims.
• Interaction matrix: pairs of already-instrumented properties (routing–traces, batching–intervals, training–calibration) whose joint behavior no committed number yet measures.
• Mutual debt: the series' closing argument: symbols owe learning their reach beyond written knowledge; learning owes symbols the guarantees that make its outputs promises rather than predictions.
• Claims matrix: a pre-registered table of advertised properties, each row resolved as toy-verified with a number or cited-only with a reason; the capstone's C1–C8 table is the series' exhibit.

Where this leads

Nowhere, and that is the point: this is the last chapter of the last volume, so the hand-off is not to another chapter but to the reader. The Series — Your Move is where the whole ladder began, and it reads differently now: the freshman's first fixpoint is your oracle pattern, and the frontier chapters you just finished are your research runway. If you want to watch the whole machine assemble again with new eyes, start where the series planted its flag, The Running Example: One Knowledge Base, Five Volumes, and follow the same thirteen entities from Horn facts to a calibrated, abstaining, trace-faithful reasoning kernel, this time noticing that at every step there was a check you could run. There still is. That is the state of the field, and it is your move.

---

Companion code: examples/frontier/suite_harness.py is the volume's regression instrument (26 committed headline values re-derived and asserted digit for digit); examples/frontier/satori_eval.py prints the C1–C8 claims table; examples/frontier/validate.py runs the full 19-check ledger this chapter quotes, and the four sibling harnesses (examples/logic, examples/symbolic, examples/neural, examples/integration, each via validate.py) supply the other 61 heartbeat checks. Run any of them with python3 from its own directory; apart from labelled wall-clock lines, every number in this chapter is their committed, byte-identical output.