Introduction to The Proofs
What This Is
The Proofs is the formal companion to Similes of Symmetry, the first volume of the Res Agentica trilogy. Where Vol I makes its argument through history and philosophy — tracing the witness structure from Mesopotamian seal impressions to Venetian notarial practice to contemporary systems architecture — The Proofs supplies definitions, theorems, and constructions through which selected parts of the argument are stated and tested under declared mathematical models.
The relationship is constitutional. Similes of Symmetry is the argument; The Proofs is the case law. Selected historical cases motivate a recurrent five-function witness pattern: binding, conditions, stakes, recourse, and composition. Recurrence supports that pattern as an institutional model; it does not prove that the functions are uniquely necessary or that they evolved independently in every setting.
The formal companion does not prove the historical thesis. It defines scoped formal objects motivated by related witness functions and establishes specified constructions and results under declared definitions and hypotheses. Its dependency chain shows what follows inside the chosen machinery, not that history could have taken no other form or that this formalization is complete or unique.
Neither work requires the other. Similes of Symmetry is designed to be read by anyone who thinks carefully about evidence, trust, and institutional design — no mathematical background required. The Proofs is designed to be read by anyone with background in category theory, type theory, or formal methods — no acquaintance with Venetian commerce required. But they are stronger together. The reader who has felt the historical argument will recognize, in the formal definitions, the structural shadows of problems that real institutions solved by trial and costly error. The reader who has verified the formal machinery will understand, in the historical narrative, why these particular definitions matter and not others.
Who This Is For
Three audiences, with different entry points.
The formal reader has background in category theory (sheaves, fibrations, adjunctions, sites), type theory (dependent types, transport, univalence), or formal methods (model checking, specification, verification). This reader can begin at Chapter 1 and read straight through. The six-part structure follows a dependency chain: each anchor builds on prior anchors, and the reading order respects the topological sort. Part introductions provide motivation and context; the formal content is self-contained.
The Vol I reader who wants to see the machinery has finished Similes of Symmetry and wants to know what stands behind the Witness Claims. Each Witness Claim in Vol I includes a formal pointer — a reference to a specific anchor in The Proofs where the formal version of the intuitive claim lives. This reader can follow the pointers selectively, reading only the chapters that address the claims they find most interesting or most dubious. The anchor table at the end of this introduction provides a complete map.
The implementer wants to build systems that satisfy the Third Mode's requirements. This reader should focus on Part V (Specification), which provides the context-graph substrate, identity maintenance, predicate packages, query semantics, and versioning rules. The appendices on implementation formats and the minimum Third Mode interface are designed for this audience. The formal reader can verify the theory; the implementer can use it.
How to Read This Alongside Vol I
Similes of Symmetry and The Proofs are coupled by the Witness Claims apparatus. Here is how the coupling works.
Each chapter of Vol I ends with a set of Witness Claims — formal-philosophical hybrids that state what the chapter's historical argument implies for the formal framework. A Witness Claim has three components:
- Intuition: A prose statement of the claim, in the register of Vol I — no notation, no formal machinery, only the felt sense of what the formal object captures.
- Formal pointer: A reference to the specific anchor(s) in The Proofs where the claim is formalized — e.g., "See A13 (Sheaf Condition), Part III, Ch. 11."
- Falsifier: A concrete scenario that would disprove the claim if it occurred — the honest admission of what would make the author wrong.
The Witness Claims are the bridge. A general reader of Vol I can treat them as chapter summaries — "here is what this chapter commits to, formally." A formal reader of The Proofs can treat them as motivation — "here is why this definition exists, historically." An implementer can treat them as requirements — "here is what a system must satisfy to earn the designation."
The numbering convention is: WC-XX-YY, where XX is the Vol I chapter number and YY is the claim index within that chapter. Each Witness Claim points to one or more A-anchors. The mapping is one-to-many (one claim can invoke multiple anchors) and many-to-one (multiple claims can invoke the same anchor).
Three reading paths:
-
Path 1: Vol I first, then Proofs. Read Similes of Symmetry cover to cover. At each Witness Claim, note the formal pointer. After finishing Vol I, read The Proofs with the pointers as a guide, checking the formal machinery against the intuitions you've built.
-
Path 2: Proofs first, then Vol I. Read The Proofs as a self-contained mathematical text. The part introductions provide enough motivation to follow the formal argument. After finishing, read Similes of Symmetry to see the historical argument that the formalism encodes — and to discover whether the formal objects capture what the history demands.
-
Path 3: Interleaved. Read Vol I Part I, then Proofs Part I. Read Vol I Part II (the computational bridge), then Proofs Parts II–III. Continue in parallel. This is the most demanding path but the one that most fully realizes the coupling.
What This Contributes
The mathematics in The Proofs is not new. The sheaf condition is due to Grothendieck. Fibrations are standard in categorical logic. Adjunctions are textbook category theory. Conservative extension is classical model theory. Transport along equivalences is the HoTT program.
What is new is the configuration. No existing text assembles these results into a single coherent framework for reasoning about systems that compose truth claims from multiple sources under coherence constraints. The individual theorems are known; the architecture that connects them is not.
Specifically, The Proofs contributes:
The sheaf condition as a coherence test. Sheaves are usually presented as objects in algebraic geometry or topos theory. Here, the sheaf condition is reread as a systems principle: local data glues into global data if and only if the locals agree on overlaps. This is the formal version of "coherence is agreement on shared territory" — a claim that applies to database merges, legal jurisdiction conflicts, sensor fusion, and institutional coordination with equal force. The novelty is not the theorem but the application domain.
Fibrations for context-dependence. The fibration $p : E \to B$, where fibers $E_b$ contain the types valid in context $b$, formalizes the observation that most predicates are not flat. "Affordable" depends on market segment. "Compiles successfully" depends on build configuration. "Best" depends on who is asking. The formalism makes context-dependence first-class and compositional, rather than an afterthought handled by ad hoc parameters.
Transport certificates for substitution. The engineering surrogate for univalence — requiring a witnessed equivalence and a transport certificate before substitution — is a practical contribution. It provides a specific, implementable discipline for when one entity may be substituted for another, replacing the current practice of either (a) requiring exact key match (too strict) or (b) allowing approximate match without tracking the approximation's scope (too loose).
The coherence cost model. The observation that coherence has a cost — and that the cost can be decomposed into local check cost, overlap check cost, witness verification cost, and version migration cost — is not a theorem but a framework. It makes the CAP theorem's insight operational: you cannot have global consistency, partition tolerance, and availability simultaneously, but you can account for the coherence budget and make the trade-offs explicit.
The proposal-certification pipeline. The separation of propose (generate scored candidates) from certify (verify with typed witnesses or structured failure) is the operational core of the Third Mode. It formalizes the distinction between "plausible" and "witnessed" that Vol I's historical argument traces from oral testimony through documentary evidence to computational systems.
The Anchor Architecture
The Proofs is organized around 32 primary anchors numbered A1 through A32, which together with six sub-anchors (A2b, A2c, A3b, A12b, A17b, A19b) form 38 formal identifiers. Each anchor defines a formal object: a definition, a theorem, or a construction. The anchors form a directed acyclic graph (DAG) generated from the explicit dependency registry and checked for missing endpoints and cycles. This is a graph of logical prerequisite, not a history of intellectual influence and not an implementation diagram for Bulla.
The six parts of The Proofs correspond to layers of the DAG:
| Part | Title | Anchors | What It Builds |
|---|---|---|---|
| I | Foundations | A1–A6 | Commitment, evidence, schema, epistemic status, coherence requirement, sense boundary |
| II | Equipment | A7–A11 | Invariants, morphisms, adjunctions, witnessed equivalence, vocabulary evolution |
| III | Coherence | A12–A16 | Context sites, sheaf condition, fibrations, logic selection, transport discipline |
| IV | Construction | A17–A21 | Predicate invention, conservative extension, proposal/certification, search, cost model |
| V | Specification | A22–A26 | Context graph, identity maintenance, predicate packages, query semantics, versioning |
| VI | Demonstrations | A27–A32 | Refusal, sense gluing, predicate acceptance, scoped equivalence, n-ary events, Third Mode definition |
The dependency graph has a longest chain (the narrative spine) that runs:
This spine traces the core argument: from commitment sets through equivalence machinery through sheaf-condition coherence through predicate invention through specification to lifecycle governance. Side branches provide essential supporting machinery — fibrations (A14), logic selection (A15), identity maintenance (A23), refusal (A27), sense gluing (A28) — but the spine carries the weight.
Each anchor has three statuses:
- Formal: Full mathematical definition with proof obligations. The main currency.
- Preformal: Informal specification that names the required properties without providing the machinery to verify them. A5 (Coherence Requirement) and A6 (Sense Boundary) are preformal; their formal machinery is delivered by later anchors (A12b/A13 for A5; A10/A16/A28 for A6).
- Engineering: An operational surrogate for a stronger mathematical principle. A16 (Transport Discipline) is the engineering surrogate for the full univalence axiom; it requires transport certificates without assuming that full univalence is computationally realizable.
The preformal and engineering anchors are honest admissions. They say: here is what we need, and here is as far as we can go without either (a) invoking machinery not yet defined or (b) assuming computational resources we do not have. The formal reader should understand these anchors as IOU notes that the text redeems at specific, stated locations.
What This Does Not Do
The Proofs does not prove that the five witness properties are sufficient for all coherence problems. That would be a completeness result, and completeness results require a precise characterization of the problem class — which this work does not provide. The claim is expressive, not exhaustive: the framework can represent a wide class of coherence problems, not that it represents all of them.
The Proofs does not provide runnable implementations. The specification in Part V is a mathematical specification — it defines operations, their contracts, and their invariants. It does not establish that an event was captured, that every relevant event was covered, that a witness persisted independently, that authority was valid, that evidence was grounded, or that a remedy is reachable. Those are additional operational and institutional layers. The appendix on implementation formats sketches what an implementation might look like; Bulla and Glyph supply separate executable and conformance surfaces. The gap between specification and implementation is real, and closing it is engineering work, not mathematical work.
The Proofs does not engage with the economic or political arguments of Volumes II and III. The coherence cost model (A21) provides a bridge — coherence has a cost, and that cost must be distributed — but the questions of who pays and who decides are the province of Factor Prime and The Sovereign Syntax. The formalism here is deliberately scoped to the epistemological question: what does it mean for claims to cohere? The institutional question — what makes coherence just? — belongs to the trilogy's later volumes.
The Proofs operates with Set-valued presheaves — the standard categorical setting where local data assigns sets of values to each context. While A2c types witnesses into three classes (decidable, probabilistic, attested) and the composition algebra tracks strength at the witness level, the broader categorical machinery — sheaves, fibrations, transport — does not natively carry probabilistic confidence bounds or attested authority chains through its constructions. The framework handles the deterministic case fully; probabilistic and attested distinctions are enforced at the witness layer but are not yet internalized in the global sheaf conditions. Extending the presheaf model to enriched settings that carry these finer distinctions through the categorical constructions is an open problem, and one whose solution would strengthen the connection between the formal apparatus and the trilogy's arguments about probabilistic AI outputs and institutional attestation.
Finally, The Proofs does not claim that category theory is the only framework that could support this architecture. Sheaves, fibrations, and adjunctions are the tools this work uses because they are the most natural for the problem — composition, context-dependence, and approximation are what these tools were designed to formalize. An alternative formalization using, say, domain theory or coalgebraic methods might yield equivalent results. The claim is not that the tools are unique but that the configuration is new, and that it works.
Notation and Conventions
The notation guide appears immediately after this introduction. Key conventions:
- All equivalences are scoped: $x \sim_S y$ for scope $S$. An unscoped equivalence claim is incomplete.
- Three levels of sameness: equality ($=$), isomorphism ($\cong$), equivalence ($\simeq$).
- Local theory $T(U) = (\Sigma, I, L_U)$ includes the logic choice $L_U$. The logic is not ambient; it is a parameter.
- Witnesses are typed per A2c: DECIDABLE, PROBABILISTIC, or ATTESTED. The composition algebra tracks strength: weakest component determines composite strength.
Reading Order
For the formal reader: Part I through Part VI, in order. The dependency chain is respected.
For the selective reader following Vol I pointers: use the anchor table above to locate the relevant part and chapter. Each chapter's opening paragraph states what it formalizes and which Vol I chapters provide the motivation.
For the implementer: Part V first, then the appendices, then Parts III–IV for the theory behind the specification.
The interludes are worked examples. They are optional for the reader in a hurry but rewarding for the reader who wants to see the machinery applied to concrete problems. The Pomegranate Boundary (Part I Interlude) is the canonical example; if you read only one interlude, read that one.