Preface — Standing at the Frontier

📍 Where we are: At the door of Volume 5 — The Reasoning Frontier. Volume 4 closed its ledger with a verdict: integration works, and it works exactly where the machinery's structure matches the problem's structure. But the same ledger named four unpaid debts (calibration, faithfulness, reasoning shortcuts, scale), and this volume exists to pay them or to say precisely why they cannot yet be paid: the same academic world, read a fifth time, as the place where every claim of the first four volumes is audited for trust and priced for scale.

Welcome to the last climb. Volume 1 built a reasoner from nothing; Volume 2 made its answers theorems; Volume 3 made its entities geometry; Volume 4 made its proofs differentiable and ended with an honest accounting of when that pays. Every one of those volumes built a mechanism. This volume builds almost none. Its business is instruments: devices that measure whether a mechanism deserves belief and whether it survives contact with size. The questions are the ones a working researcher actually faces. When the system answers, what is the smallest honest reason for the answer, and is the explanation it offers the reason it used? When it is right, is it right for the right reason, and how many wrong reasons produce the same score? When it says 0.9, is it right nine times in ten, and does it know when to say nothing? When the knowledge base grows a thousandfold, which of our algorithms come along, and what do the survivors trade away? And when a fixed-depth neural network hits a provable ceiling, what exactly buys the lost depth back? The frontier is not a bigger machine. It is the discipline of auditing the machines we already have.

The simple version

Imagine a new drug that cures the lab mice every time. Nobody ships it on that evidence. First come the trials that ask why it works, because a compound that cures through a side effect will fail the moment the side effect is absent (right answer, wrong reason). Then the label must state the real risk, not the marketing number, and a doctor must know when not to prescribe (calibration and abstention). Then the factory question: a synthesis that works in a beaker may be unaffordable at a million doses, and there are two rival production strategies with opposite costs (scale). Finally, the trial itself gets audited: did it measure the disease, or just the mice's habits (benchmarks)? Volume 5 is that entire regulatory gauntlet, run on the reasoning systems of Volumes 1 through 4. The machine already works. This volume decides whether to trust it, and what it costs to run.

What this volume covers

Volume 5 is one continuous audit in nine parts. Each part builds one instrument and answers one question:

Part	Theme	The question it answers
I · Proofs, Faithfulness, and Trust	justifications and Reiter's hitting-set tree; erasure-tested faithfulness; rule extraction	What is the smallest honest reason for an answer, and is the story a system tells the reason it used?
II · Identifiability and Reasoning Shortcuts	shortcut counting; why accuracy never certifies meaning; rsbench's concept-quality instruments	How many ways can a model be perfectly right for the wrong reason, and can you count them before training?
III · Calibration, Uncertainty, and Abstention	temperature scaling and ECE; Chow's rule and the risk-coverage curve	Can a confidence number be made to mean something, and when should a system refuse to answer?
IV · Scale and Systems	materialization versus rewriting; the batched GPU fixpoint; the work-depth trilemma	What does the closure cost at a million facts, and what does computing it fast trade away?
V · Neural Depth: Chain-of-Thought and RL	the TC⁰ ceiling; scratchpads that recover P; verifier-gated reinforcement learning	Why does a fixed-depth transformer hit a wall, and how do decode-time steps and verifiers buy the depth back?
VI · Benchmarks and Evaluation	seven difficulty axes beyond completeness; suites and simulators; the entailment gap	What must a benchmark vary before it measures reasoning rather than recall?
VII · The SATORI Capstone	symbolic attention; one operator, four properties; the C1–C8 claims matrix	Can one lattice operator carry both classical reasoners exactly, and which of its claims survive the evidence?
VIII · The Research Runway	the G1–G8 gaps; blind spots and first steps	Where exactly does the field's knowledge stop, and what is the first experiment past that line?
IX · The Verdict	the whole ledger	After five volumes, what is the honest state of neuro-symbolic AI?

Who this volume is for

This is written for a graduate student ramping toward active research, the series' ceiling. It assumes everything the ladder has built: Volume 1's forward chainer and unification, Volume 2's EL++ TBox and its completion rules, Volume 3's embeddings and the filtered-ranking protocol, Volume 4's weighted model counting, gradient semiring, and query DAGs. Nothing else arrives as a black box. The companion suite examples/frontier/ implements every instrument in plain NumPy with every gradient derived by hand in a comment above the line that computes it, imports the prior volumes' machinery rather than retyping it, and is sealed by validate.py, an acceptance harness whose 19 competency checks pass 19 of 19 on the committed code in about 56 seconds. Every module seeds its randomness, so every number quoted in every chapter reproduces byte-identically with python3 <module>.py.

The thesis: accuracy certifies neither meaning nor deployability

Here is the conviction the volume turns on. A test-set score, however high, is a statement about outputs, and trust and scale are statements about everything the score cannot see. The volume makes this precise twice. On the trust side it is a counting fact: on the suite's smallest concept-learning world, a symmetry group of order 4 makes 15 of the 16 loss-global optima produce perfect task labels from mis-grounded concepts, so a perfect score is evidence of correct meaning at rate one in sixteen. The same blindness reappears as an unfaithful explanation (a 0.961-accurate classifier whose attention story flunks the erasure test) and as an uncalibrated confidence (a shortcut model posting task accuracy 1.000 beside concept accuracy 0.750 and an expected calibration error of 0.247). On the scale side it is an accounting fact: the correct answer computed by 510 sequential waves and the correct answer computed by 10 parallel squarings are the same answer at a 10,270-fold difference in total work, and neither cost appears anywhere in a correctness proof. Trust must be measured, and scale must be counted. Every chapter of this volume builds the instrument that does one or the other, states the theorems it imports (TC⁰ containments, #P-hardness, the shortcut-counting results) with attribution and without pretending to reprove them, and runs the instrument on our world.

The running example, read a fifth time

The world does not change; the reading does. Volume 1's kb.py still holds the 23 base facts and the Horn rules whose closure completes in three waves; Volume 2's ontology still holds the EL++ TBox; Volume 3's kg.py still holds the split and the ranking judge; Volume 4's suite still holds the differentiable machinery. The fifth reading points instruments at all of it. The hitting-set tree finds all 7 minimal justifications over 4 entailments, checked against a brute force over all 16,384 axiom subsets. Rule extraction reads the gold composition advises∘advises out of trained weights at confidence 0.999, and in the same breath shows a 16/16-faithful extraction from a biased network that is right about the world only 8 times in 16. A verifier-gated selector answers 92.9% of queries with zero wrong answers, purchased by abstention on the rest. The EL fixpoint, vectorized into boolean matrix algebra, matches Volume 2's oracle cell for cell and closes 100 TBox variants in one stacked tensor pass. And the capstone's single lattice operator reproduces both classical oracles exactly, 47 of 47 Horn facts and 46 of 46 EL subsumptions, before facing the eight claims it was built to test. One tiny world, five readings, and the last reading is the audit.

One academic world under audit: the trust instruments on the left, the scale instruments on the right, the depth ceiling above, and the nine-part climb of the volume laid out beneath, ending in an arrow that points past the book at the reader's own research. Original diagram by the authors, created with AI assistance.

Trust begins with a minimal proof

Part I starts where trust has to start: with reasons small enough to inspect. A justification is a minimal set of axioms that entails a conclusion, Reiter's hitting-set tree enumerates all of them, and a repair is the dual object, a smallest deletion that provably kills an unwanted entailment. Faithfulness then asks the harder question about learned systems: an explanation is honest only if removing what it points at removes the answer, and the erasure test quantifies this, catching a highly accurate classifier whose attention weights tell a story its gradients do not support. Rule extraction closes the part with the sharpest lesson in it: an extracted rule can be perfectly faithful to the network and still wrong about the world, because fidelity and truth are different measurements.

Right for the wrong reason: the shortcut mathematics

Part II gives Volume 4's "right for the wrong reason" observation its mathematics. A reasoning shortcut is a grounding of concepts that satisfies the training objective while meaning the wrong thing, and the deep result is that shortcuts can be counted in advance: symmetries of the label-generating process fix the number of loss-equivalent optima, our world's order-4 group makes fifteen of sixteen optima mis-grounded, and each added disambiguator (a reconstruction term, a concept label, an intervention) shrinks the orbit by a factor the theory predicts exactly. The rsbench chapter turns the counting into practice, rebuilding the concept-quality instruments in miniature and separating models that no task metric can tell apart.

Confidence with a meaning, and the right to say nothing

Part III repairs the number every downstream consumer actually reads: the confidence. Calibration demands that among all answers scored 0.9, about nine in ten be correct; expected calibration error measures the shortfall, and temperature scaling, a one-parameter fix, cuts our probe's ECE from 0.0245 to 0.0167 without moving accuracy at all. Abstention then makes uncertainty actionable: Chow's rule says when refusing to answer beats answering, the risk-coverage curve prices every abstention policy, and the part's payoff is the verifier-gated selector, which converts abstention plus a symbolic checker into a system that answers 92.9% of queries and is never wrong on the answers it gives.

The price of the closure: scale

Part IV asks what happens when the academic world stops being tiny. Materialization computes the closure once and answers by lookup; rewriting stores nothing and expands each query at ask time; the suite runs both against an SLD oracle, counts the storage (47 facts against 23), and walks the maintenance problem (DRed overdeletes 2 facts and re-derives exactly 1) and the expressibility wall where rewriting fails. The GPU chapter vectorizes the EL fixpoint into batched boolean matrix multiplications that match the oracle cell for cell, and the work-depth chapter counts the trilemma honestly: squaring closes a 512-step chain in 10 matrix multiplications where semi-naive evaluation needs 510 waves, at a 10,270-fold premium in total work.

The depth ceiling, and buying depth back

Part V is the volume's deepest imported theory. Fixed-depth transformers sit inside the circuit class TC⁰, and problems like iterated composition provably do not, so a hard ceiling exists; the companion does not reprove the theorem, it measures the cliff, watching fixed-depth networks fail at exactly the lengths the theory predicts while a depth-scaled control keeps tracking. Chain-of-thought is then the escape: each decoded step re-enters the network, depth becomes proportional to steps, and the scratchpad model stays exact out to 32 steps where its fixed twin cliffs at 5. Verifiers close the part: a symbolic checker gating a proposal policy cuts wrong derivations from 0.247 to zero, and using the verifier as a reward signal lifts the policy's exact-proof rate from 0.205 to 0.535.

Benchmarks as instruments

Part VI turns on the evaluation itself. Completeness is only one axis of difficulty; the suite exhibits seven more, one gadget each, including a chase that never saturates and a query whose proof width pays 1,024 leaves at equal depth. The suites chapter assembles five instruments into a miniature benchmark harness that re-derives 26 committed headline digits and separates accuracy-tied model pairs on every axis. The entailment-gap chapter delivers the part's verdict number: a soft reasoner that scores 98.96% on its test set is only 71.6% and 48.6% logically consistent under expansion and paraphrase, while the translate-then-prove pipeline is 100% consistent on everything it parses.

The capstone: one operator, eight claims

Part VII assembles the series into SATORI, the research program this book orbits: reasoning as a single burst of symbolic attention, one lattice operator that reproduces Volume 1's Horn closure and Volume 2's EL completion exactly, with annotation soundness carried through at threshold τ. Then the volume does to SATORI what it has done to everyone else: the C1–C8 claims matrix is evaluated instrument by instrument, five claims toy-verified with committed numbers, three honestly marked cited-only, and the wedge between what is demonstrated and what is conjectured is drawn in ink.

The runway and the verdict

Parts VIII and IX end the series facing forward. The gaps chapter names G1 through G8, the places where the field's knowledge actually stops, each stated as a falsifiable question with the instrument that would test it. The methods chapter is a working researcher's checklist: the blind spots this volume's audits keep finding, and the first experiment to run past each one. The final chapter delivers the promise in the series' title, an honest verdict on neuro-symbolic AI, argued from the five volumes' committed evidence rather than from enthusiasm.

Where this leads

Trust starts with the smallest object that can carry it: a proof with nothing wasted in it. The first chapter, Justifications: Minimal Proofs and Pinpointing, defines a justification as a minimal entailing axiom set, builds Reiter's hitting-set tree to enumerate all of them, proves the enumeration correct, and runs it on the academic world, finding all 7 minimal justifications behind 4 entailments, verifying the enumeration against a brute force over 16,384 subsets, and checking every repair against the reasoner. The audit begins with the auditor's own tools.