Interlude I-C: What We Claim
Aa
This interlude states the novelty boundary: what The Proofs claims, what it does not, and what would falsify the contribution. It serves as the formal commitment register for the entire work.
What We Claim
Part I has diagnosed a gap. Before Part II begins the recovery, we state precisely what The Proofs contributes—and what it does not.
What Is Not New
The mathematical machinery we employ is established. Sheaf theory supplies the exact local-to-global gluing condition. Dependent types and fibrations provide established ways to represent context dependence; the particular transport and adjoint constructions require their stated hypotheses. Conservative extension, a cornerstone of model theory since Robinson and Shoenfield, concerns preservation of consequences in the old language. Proof-carrying code and certificates, introduced by Necula in the 1990s, show how artifacts can witness properties and survive inspection. Schema evolution and semantic versioning, familiar to any database or software engineer, provide compatibility classes for changing interfaces.
We are not inventing these ideas, and we claim no priority over them. Readers familiar with categorical logic, type theory, or formal methods will recognize the components.
The Proposed Contribution
The contribution proposed here is architectural: connect evidence, scope, substitution, admission and later use in a single specification. Priority for that combination has not been established. The nearest antecedents include proof-carrying code, database provenance, schema evolution and sheaf-based information integration; Appendix L examines the relevant comparison.
First, the specification asks an implementation to preserve the grounds of its local-to-global claim. In the effective exact fragment, an unequal pair of restrictions can be returned as a checkable failure. A matching family without an established amalgamation, or a check that did not finish, needs a different result. Recording those differences is a design requirement; it is not a new sheaf theorem.
Second, equivalence is accompanied by a scope, maps and property footprint. Mathematics already studies restricted and indexed equivalences. The operational question is which evidence a receiving computation must possess before making this particular substitution, and what it must refuse to infer when that evidence is missing.
Third, predicate admission is followed through revision and use. Tests, model-theoretic conditions, authority and compatibility answer different questions. The proposed lifecycle connects them without making a successful test discharge every other obligation. Ordinary systems can already implement parts of that discipline; the synthesis must earn its value in the connections.
What We Contribute
In one sentence: we propose a discipline for carrying a claim’s grounds into the operations that admit, translate and reuse it.
The objects that constitute this layer are:
| Object | What It Does | Where Defined |
|---|---|---|
| Commitment Set | Tracks what a system has asserted | A1 (Ch. 1) |
| Witnessed Assertion | Binds claim to evidence | A2 (Ch. 2) |
| Sheaf Condition | States when matching families have a unique amalgamation | A13 (Ch. 11) |
| Obstruction Witness | Records why gluing failed | Ch. 11 |
| Scoped Equivalence | Bounds substitution to declared contexts | A30 (Ch. 28) |
| Predicate Acceptance | Gates new predicates with tests + lifecycle | A29 (Ch. 27) |
| Minimum Interface | Specifies ten operations with artifacts and unresolved implementation obligations | Appendix I |
The artifacts make the obligations inspectable. Their contribution does not depend on being the first artifacts of their kind.
The Test
A skeptical reader may ask: "Is this just standard category theory dressed up for engineers?"
An implementation would have to show what the proposed connections add: which error it detects or exposes, which decision the evidence changes, and what burden the additional checking creates. Its comparator should include systems that already preserve the relevant information. Failure to improve that comparison would weaken the practical contribution without making the borrowed mathematics false.
The remaining chapters specify the discipline and distinguish the constructions supplied from the obligations still open.