7. Capstone theorems — what the calculus can do
A reader who has followed the chapters so far knows what the calculus is: a kind is a type index, two kinds meet only under a witnessed law, a boundary is declared and then decided, and a model carries its attestations as hypotheses. The question a reviewer asks first is a different one: what can the calculus do? What guarantee does a model earn by being written in it — stated as a theorem whose hypotheses the build discharges and whose conclusion a reviewer can use without reading the model? Three theorems answer it, one per layer of the calculus — the provenance layer, the computation layer and the dimension layer, laid out below — read through the taint-tracking paradigm:
-
The seal of a module. Once a module's inputs, constants and attestations are declared, no other raw datum reaches its outputs: every leaf of an output's pedigree is a declared source. Stated over the metrological provenance hypergraph the build harvests from the module's members; its hypotheses are the two kernel-decided judgments the build already pins per boundary.
-
The seal of the computation. The same guarantee for the computation itself, at every carrier the module is instantiated at: an output depends only on the sources the hypergraph names for it, every constant it uses is one the audit lists, and every kind change in the computation sits at a declared crossing. Stated over the computational tape graph of the tape a carrier-generic module records, related to the provenance hypergraph by a kind-transporting weak bisimulation.
-
Dimensional homogeneity of the kind algebra. Every derived kind in a well-formed provenance hypergraph carries the dimension the family rules compute from its operands, so the dimension functor is a homomorphism along every occurrence — not only along the edges an interaction algebra curates.
Four named objects appear in these statements, and this chapter keeps them apart. The metrological provenance hypergraph is the kinded object the first capstone is stated over, harvested from the source, and it is where every kind originates; the value-flow digraph is its binary shadow, the graph reachability is proved on. The tape is not a graph but a record — the sequence of carrier operations a module writes when evaluated at the recording carrier — and the computational tape graph is the directed acyclic graph that record determines, the object the second capstone relates to the provenance hypergraph; it carries no kinds until the kind-transporting weak bisimulation transports them. None of the four is the blueprint dependency graph drawn at the end of this document, which is a picture of the document itself.
This chapter was written blueprint-first, in the discipline the proved spine records after the fact: each theorem was stated informally with its hypotheses and its proof sketched against the declarations that existed, and the declarations were then written to the sketches. Every node now links the declaration that discharges it, and the ledger at the end records what the sketches priced and what remains an instrument rather than a theorem. Two rules govern every statement below. Non-vacuity is a deliverable, not a hope: each capstone owes three witnesses — an instance whose hypotheses the kernel decides, a mutant that fails the hypothesis and the conclusion, so that the hypothesis is shown to carry the weight, and a pinned axiom profile. The seal is no undeclared entry, not no entry: raw data enters a sealed module through its declared gates — a checked ingest, a constant mint, an attestation with its reason — and the theorem's content is that the build's list of gates is complete.