Appendix A — Method, notation, and reading order

Persuasion is what you need when you don’t have a proof, so this book runs on apparatus, and the apparatus has rules. A statement’s sources come in the three kinds the preface names: spec definitions, earlier propositions, checkable observations. A fourth kind corroborates but never serves as premise — witnesses, documents that stated as norms what this book derives as theorems. Strike every witness and no proof changes. One claim is deliberately unprovable, flagged where it stands: the Transposition Thesis of Chapter 5, the bridge between the formalism and the web itself. It is secured there and in the appendices, proved never. Disagreement belongs at the bridge; given the requirements, the theorems add no premise of their own.

The shape of the whole is Chapter 2‘s method, run at book length: analysis and synthesis, in the geometers’ sense. Parts II–III strip the web application as found and derive what its parts must be. Part V builds the application space back from the derived parts. The two directions meeting exactly is the book’s proof. Part IV, between them, audits what the industry runs instead, ending with the derived stack itself. There is no editorializing, only scores against Part II’s seven properties: three requirements on state (R1–R3), four separations on architecture (S1–S4). Its closing chapter is the completed table.

If you have ever read a type signature, you have read every formula in this book — × is a tuple, → a function; the crib below translates the rest. Proofs fold: the claim stays in the text, the argument opens on demand. Results carry names, because prose argues by name; the numbers let the appendices argue by label.

Sets, tuples, total functions, and composition ∘ — first-year material, as promised. Two conventions: ⟦·⟧ is a denotation function and always someone else’s, cited from the governing specification, never defined here; t names the arrange term (S2), so time is written τ. The numbered apparatus is as follows. R1–R3 are the requirements on state, with R4 (attribution) added in Chapter 9. S1–S4 are the separation properties of a factorization. The B-conditions are the formalizations in Appendix B. Propositions are chapter-numbered.

The symbol crib, for readers who live in code:

symbol reading in code
A × B a pair: an A and a B a tuple; a two-field record
A → B function from A to B (a: A) => B
𝒫(A) all sets of As Set<A>
∪, ∩, ∖ union, intersection, difference union(), intersection(), difference()
⊔ disjoint combination of independently asserted structures two sources’ data, side by side
∘ composition, right to left compose(f, g)
⟦q⟧ what q means, per its spec the standard defines what your query returns, not your driver
s ⊕ s′ merge two states set union of their facts — the union law (5.1)
s ⊕ s = s idempotence re-merging is a no-op; safe to retry
(D⁻, D⁺) a delta a diff: deletions, additions
≅ isomorphic same shape; lossless conversion both ways
≡ logically equivalent equal after normalizing — same meaning, maybe different syntax
τ time a version, a timestamp
I the set of URIs globally unique identifiers (RFC 3986)
V atomic literal values, disjoint from I strings, numbers, dates — the leaves
O the set of origins a scheme–host–port triple (RFC 6454)
I∣o the URIs under origin o one party’s region of the namespace

Reading order: Parts I–III go linearly. Chapters 10–14 need only Chapter 8 and go in any order, then Chapters 15 and 16. Part V needs nothing past Part III. Three tracks, if you are choosing a path:

The formulas are skippable and the prose carries every argument; the formulas make the prose auditable.

And the named results, so prose and apparatus can find each other:

name label where
the trivial factorization Prop. 4.2 Ch 4
properness Def. 4.3 (S1–S4) Ch 4
the analysis theorem Prop. 4.4 Ch 4; B.5
independent evolution Prop. 4.5 Ch 4; B.6
the union law (5.1) Ch 5; B.1
the arity argument Prop. 5.2 Ch 5; B.2
the shape of a fact (5.3) Ch 5; B.2
the uniqueness theorem Thm. 5.4 Ch 5; B.3
the classification a thesis, deliberately unnumbered Ch 6
the canonical serialization (canon) Prop. 6.1 Ch 6; B.8
the delta normal form Prop. 7.1 Ch 7
forms as inverse transforms Prop. 7.2 Ch 7
one algebra, both directions Prop. 7.3 Ch 7
the five moves Prop. 7.4 Ch 7
the homomorphism Prop. 8.1 Ch 8; B.7
the synthesis theorem Thm. 8.2 Ch 8; B.8
the bill for anonymity Prop. 9.1 Ch 9
the erasure argument Prop. 9.2 Ch 9
the dataspace (17.1) Ch 17; B.9
nothing else to vary Prop. 19.1 Ch 19
the Transposition Thesis a thesis, deliberately unnumbered Ch 5; B.2