Appendix B — Proofs

Prop. 5.2 and Thm. 5.4 come first, reached through B.1’s formalization of R2. They are the two results everything downstream rests on, so they get the most care. Then come independence (B.4), analysis (B.5), timelines (B.6), the homomorphism (B.7), synthesis with genericity made exact (B.8), and federation closure (B.9).

B.1 R2, formalized — and the representation lemma

Chapter 5 argued in prose; a proof needs the requirements as mathematics. The translation is itself the honest step: every choice below is a numbered condition with its one-line justification from the web, so that rejecting one is a precise act rather than a suspicion. Chapter 16’s Properness Table already tells you what each rejection costs. Conditions carry the number of the requirement they formalize — B-2a–e for R2, B-1 for R1, B-3 for R3, B-0 for the form-level ground — hyphenated, to keep condition B-1 apart from section B.1 and its lemma.

Fix I, the URIs (RFC 3986), and V, a set of atomic literal values disjoint from I. A state model is a pair (M, ⊕): a set of states and a composition. R2 — composition among parties who have never communicated — formalizes as four laws and one closure condition:

(B-2a) Totality. ⊕ is defined on every pair of states. Composing may never require a compatibility check, because checking is coordinating.
(B-2b) Order-freedom. ⊕ is associative and commutative. States arrive from independent parties in no agreed order; if order mattered, the order would have to be agreed.
(B-2c) Idempotence. s ⊕ s = s. On the web copies are free and copies of copies are unmarked; a state received twice is the state received once. A model that counts arrivals must know which arrivals are “the same sending” — and that knowledge is coordination.
(B-2d) Atomicity, no emergence. Write s ≤ s′ for s ⊕ s′ = s′ (“s says at most what s′ says”). M has a least element ∅ — the party with nothing to say. An atom is a minimal state above ∅. Require: every state is the join of the atoms below it, and atoms(s ⊕ s′) = atoms(s) ∪ atoms(s′). In words: a state says exactly what its atoms say, and composition neither creates nor destroys atoms. This is Chapter 5’s “a fact must carry its full meaning with it,” as algebra. If a combination of states could mean more (or less) than its facts together, the surplus would live in an arrangement. Some union would fail to preserve it, and the parties would have to agree on its interpretation — coordination again.
(B-2e) Accumulation. Every directed family of states has a join, with atoms of the join the union of the family’s atom sets. This one is bookkeeping, not a transposed law — which is why Chapter 5’s table has four rows, not five. The four laws govern the merge of finite messages; a store keeps receiving, and B-2e says the model has a state for the limit of any such accumulation.

Lemma B.1 (Representation). A state model satisfying B-2a–e is isomorphic to (𝒫(A), ∪), where A is its set of atoms. Proof. Map s ↦ atoms(s). Injective: by B-2d every state is the join of its atoms, so two states with the same atoms are the same join. Surjective: a finite set of atoms is realized by its join (B-2a supplies the join; B-2d‘s second clause guarantees the join’s atoms are exactly the atoms joined), and an arbitrary set is the directed join of its finite subsets’ realizations (B-2e supplies that join and its atoms). Homomorphism: atoms(s ⊕ s′) = atoms(s) ∪ atoms(s′) is B-2d verbatim. ∎

(Without B-2e the lemma holds in the finite: the atom map embeds M into 𝒫(A), and its image contains every finite set of atoms — the version that carries the operational content, since messages are finite. B-2e is exactly what the full powerset costs, and it is now on the bill rather than in a remark.)

Rename Fact := A, and (5.1) is proved from the named conditions. (A scope note for readers arriving from deployed RDF: over ground atoms, composition is set union exactly. With blank nodes, RDF itself distinguishes union from merge — standardize-apart, the Merging Lemma of RDF Semantics (2004) — and the laws hold up to logical equivalence, as Prop. 9.1 states and measures. The characterization is over ground atoms; 9.1 is its honest extension.) The exits are visible already — each law rejected is a deployed model, catalogued after Theorem 5.4 in B.3.

B.2 Proposition 5.2 — the arity of a fact

Prop. 5.2 (restated). The minimal self-contained fact is a triple.

What remains free is the structure of an atom. Three more conditions name what Chapter 5’s prose used:

(B-0) Finite, self-interpreting atoms. An atom is a finite tuple over I ∪ V, one length per model — a reading that dispatched on length would be two readings — and its meaning is a fixed, universal function of the tuple alone. This is B-2d again, at the atom’s own scale: no atom means by way of its neighbors, and no atom’s reading varies by domain or by party. One reading, agreed once, for everything. (Agreeing on that single reading is itself an act of coordination — performed once, about form, never about content. That is what a specification is. R2 forbids per-domain agreements, and licenses exactly this one.)
(B-1) Faithful universal encoding (R1). For every finite relational structure D — entities and relations, both named; the shape every deployed data model reduces to — there is an encoding enc(D) ⊆ Fact, injective up to isomorphism, and compositional: independently asserted structures encode independently, enc(D ⊔ D′) = enc(D) ∪ enc(D′).
(B-3) Global names (R3). Names occurring in D are drawn from I and occur verbatim in enc(D) — references must survive encoding, or cross-source references stop matching at exactly the moment sources encode independently.

Arity 1 fails. A 1-tuple (x) occurs or does not occur; by B-0 its meaning is a function of one name. For enc to distinguish R(a,b) from R(b,a) — same names, different structure — some atom must mean a whole proposition. A bare name can only mean a proposition by assignment: its owner publishes, somewhere, what the name stands for. But the publication must itself be stated in some model, and if that model is again bare names, the regress never grounds. A model of pure names is parasitic on a model of higher arity. Naming is not asserting.

Arity 2 fails. By B-0 a pair carries one fixed universal reading — some single relation between its components; a reading that varied per pair would be per-pair agreement, which is coordination. One fixed binary relation is expressively a single unlabeled directed graph, and B-1 demands arbitrarily many distinguishable relations over the same entities: R(a,b) and S(a,b) must encode differently, yet the pair (a,b) is all a pair can say. The remaining escape is the gadget: encode the relation’s identity as a shape built from fresh nodes around the edge. Two conditions kill it. First, shapes must be assigned to relation names by a global scheme over the unbounded namespace I — a label registry, which is a central schema authority, the exact thing R2 excludes. Assigning shapes by dereference instead reruns the arity-1 regress. Second, inside a gadget the individual pair means nothing until the whole shape completes. Atoms have stopped carrying their meaning, and B-2d is violated at atom scale. Two parties independently asserting gadget-encoded facts about shared entities can union into a state whose decoding is ambiguous. The pair’s failure is Chapter 5’s line made precise: (employee42, "2026-07-08") is hired-on, or fired-on, or born-on — the meaning lives outside the fact.

Arity 3 suffices. The one universal reading: (s, p, o) asserts the relation named p holds of s and o. The atom names its own relation — position two supplies what arity 2 lacked, and B-3 draws it from I. The encoding, case by case. A binary fact R(a,b) becomes (a, R, b). A unary classification P(a) becomes (a, kind, P) for one distinguished attribute kind, licensed like the reading itself: one form-level convention, agreed once. An n-ary fact R(a₁, …, aₙ) becomes a fresh entity e with atoms (e, rel, R) and (e, roleᵢ, aᵢ), the role names published by R’s owner alongside R. Minting fresh names is free, and every party owns a namespace to mint in (RFC 3986’s authority component). Note the contrast with the gadget: here every atom still means alone — (e, role₂, a₂) says, completely and context-freely, that e’s role₂ is a₂ — and the n-ary fact is the conjunction of its atoms. Accumulation, never emergence. Faithfulness and compositionality are routine to check; injectivity is up to the choice of fresh names, a degree of freedom Chapter 9 meets again under its deployed name.

Minimality pins three. Arities 1 and 2 fail; arity 3 succeeds; and every arity above 3 also succeeds — quads meet every condition. The conditions bound arity from below only. What selects three is parsimony: any k-model with k > 3 encodes into the 3-model by the same decomposition just given, so the 3-model is the minimal universal one, and minimality is stated in Theorem 5.4’s hypotheses rather than smuggled. The wider tuples are a door, and one requirement opens it: make facts themselves attributable — R4 — and the minimum becomes four (Chapter 9).

Positions, typed. Position 2 lies in I: the reading makes it a relation name whose meaning must hold across independent sources. Shared meaning without coordination is ownership plus documentation, which only I provides; a literal owns nothing and dereferences to nothing. Position 1 lies in I: subjects are where facts accumulate across sources, accumulation is join-on-subject, and joining beyond a single source requires reference. A literal denotes itself — you do not add facts to the number five. Position 3 lies in I ∪ V: descriptions must terminate in values, or no fact ever touches data. Literal subjects add no expressive power — any structure “about” a value factors through the entities that carry it — so minimality removes them. This yields (5.3): Fact = I × I × (I ∪ V). ∎

Scope, and the history that shapes it. The mathematics here has a pedigree and a trap, and both belong on the table. As pure relation theory, the shape of this result is Peirce’s Reduction Thesis: dyads insufficient, triads sufficient, higher arities decompose. The thesis was conjectured in the 1880s and proven in modern form by Burch (1991), Dau & Hereth Correia (2006), Hereth Correia & Pöschel (2011), and Koshkin (2022–2025). The arity theorem is not new mathematics, and this appendix does not claim it. What is claimed is the derivation of its hypotheses from web-state axioms, and the typing of its positions into I — no work in the Peirce line mentions the web or its data models.

The trap: the insufficiency of pairs is operation-relative, and stated without qualification it is false. Löwenheim (1915) and Quine (1954) proved that under unrestricted set-theoretic pairing, every relation of every arity reduces to dyads — the same fresh-entity move this proof uses to decompose n-ary facts, pushed one step further. What blocks the push here is B-0 and B-2d: the pairing reduction manufactures atoms that no fixed universal reading interprets alone — pairs that mean only via their neighbors. That is the gadget escape, closed above. In Peirce’s setting, the analogous restriction has been accused of gerrymandering (Skidmore 1971; Koshkin 2022): drawn where it must be for triads to win. In this setting the accusation has an answer the Peircean one lacks. The restriction is the Transposition Thesis’s fourth row: no meaning survives in arrangement. That row is a deployed invariant of the web, adopted for reasons that predate any question about arity. The web drew the line, not the theorem.

One prior assertion completes the record. Robertson (2005) wrote of RDF that ternary relations are “the minimal … way to encode semantics wherein metadata may be treated uniformly with regular data” — asserted as motivation for a triadic query algebra, underived. This appendix is, among other things, the derivation that assertion was owed.

B.3 Theorem 5.4 — uniqueness, assembled

Theorem 5.4 (restated). Isomorphism of state models here is reading-preserving: the bijection carries ⊕ to ⊕ and atoms to atoms, and on atoms it acts position by position, holding names and values fixed — it may permute tuple positions and relabel nothing. Bare ⊕-preserving bijections are too coarse to carry the claim: any two powersets of equinumerous atom sets admit one, and the widened tuples would pass. The content lives in the structured notion. Let (M, ⊕) satisfy B-2a–e, B-0, B-1, B-3, and among such models be arity-minimal. Then (M, ⊕) ≅ (𝒫(I × I × (I ∪ V)), ∪), reading-preservingly.

Proof. Lemma B.1 gives M ≅ 𝒫(A) with ⊕ carried to ∪. B.2 gives A = I × I × (I ∪ V) up to permuting positions: arities below three cannot satisfy B-0/B-1/B-3, arity three can, and minimality excludes the rest. The product is full because B-1 refuses no structure — every triple over the typed positions is enc of some D, so every triple is an atom. Compose the isomorphisms; each fixes entries and at most permutes positions, so the composite is reading-preserving. Uniqueness is up to the permutation of tuple positions — a renaming of the reading, and not a distinction worth disputing. ∎

The exits, restated with their numbers. Reject B-2d and meaning moves into arrangement: the document family — XML, JSON — audited in Chapter 10. Reject B-3 and names stop at the database boundary: the relational world and its integration industry, Chapter 13. Reject B-1 and the format serves one domain: the per-API bridge industry, Chapter 13 again. Reject B-2c and you are modeling events; their replay into state must land in a model satisfying the rest, and the exit returns you here. Reject minimality upward and you have quads — the one exit that leads deeper in rather than out, Chapter 9. Each exit has a name, a chapter, and a cost.

B.4 Independence of the conditions

None of B-2a–e is redundant, and the proof is the standard one: for each condition, a model satisfying the other three (suitably restated where the dropped law is presupposed by another’s phrasing) in which the characterization fails.

Drop B-2a (totality). Relational union under schema compatibility: composition defined only where schemas agree. Order-free, idempotent, and atomic where defined — and composing across independent parties now requires the compatibility check, which is the coordinator returning. States are schema-indexed families, and Lemma B.1’s target is gone.
Drop B-2b (order-freedom). Event logs under append, deduplicated by entry identity: total and idempotent — and the composite depends on interleaving, so two parties’ logs have no canonical join. The structure is a monoid, and the representation fails.
Drop B-2c (idempotence). Multisets under multiset union: total, order-free, atom-determined — and s ⊕ s ≠ s semantically, because arrival counts. The representation lands on ℕ^A, and federation now needs to know which arrivals are “the same sending” — provenance machinery, which is coordination.
Drop B-2d (atomicity). (ℕ, max) — Bloom^L’s own lmax lattice: total, order-free, idempotent, with least element 0 and sole atom 1. The state 2 is not the join of the atoms below it, so states are no longer determined by their atoms and the representation fails. Trees under meaning-bearing grafting fail the same way at scale, and Chapter 10’s audit is the deployed consequence.
Drop B-2e (accumulation). The finite subsets of an infinite A under union: all four laws hold, and the store has no state for the limit of an unbounded accumulation. The representation lands on the finite-subsets lattice, short of the powerset.

Each law’s countermodel is one of Chapter 5’s exits, its non-redundancy now proved: remove any law and the uniqueness theorem loses its target. All four are load-bearing, so the work of the characterization is distributed — no single condition smuggles the conclusion. For B-2d the literature supplies a deployed witness. Bloom^L (Conway et al., 2012) generalizes coordination-free programming from relations-under-union to arbitrary lattices with associative, commutative, idempotent merge — counters, maps, booleans. It demonstrates in running code that the merge laws alone leave the data model open, exactly as this section claims. ∎

B.5 The analysis theorem (Prop. 4.4)

Formalize the hypothesis first. Finite dependence: for every request r there is a finite set K(r) ⊆ Fact — a window — with read(r, S) = read(r, S ∩ K(r)) for all states S. This is what “depends on State only through some finite part” means, and it is what sets the theorem’s scope: a read that inspects the whole infinite state at once has no window and gets no factorization. Deployed reads have windows — a response is finite, computed in finite time from finitely many facts.

Choose, for each r, an inclusion-minimal window (one exists inside any window by finiteness; when several minimal windows exist, fix any — the construction below works for every choice, so the choice is immaterial). Chapter 4’s sketch said “the minimal fragment”; the honest article is “a minimal fragment, fixed henceforth.”

Now the construction. One wrinkle must be handled in the open: the output may depend on r beyond the selection — the same data renders differently for a different Accept-Language — and arrange is forbidden by S1 from seeing r. The repair uses the derivation’s own move: a request is a finite named structure, so by B-1 it encodes as facts. Define:

select(r, S)  =  (S ∩ K(r)) ∪ enc(r)
arrange(D)    =  canon(read(dec(D)))      dec: recover (r, S∩K(r)) from D
present       =  the rendering of a canonical tree as Doc

select is a function of (r, S), as typed. dec is well-defined because enc is injective and its facts are disjoint from K(r) (mint them under a reserved authority, which costs nothing). arrange is a function of D alone: everything it needs — the window’s facts and the request’s — arrived in its argument, so S1 holds by construction rather than by discipline. canon is overloaded here, deliberately and in the open: Chapter 6 typed it on states, but its argument above is read’s output, a Doc. At this type canon means the document’s canonical tree, and present is its inverse, rendering the tree back unchanged. present sees a tree, never the data. Composing: present(arrange(select(r, S))) = read(r, S ∩ K(r)) = read(r, S) by finite dependence. ∎

What this proof does and does not give: it gives S1 and the shape — every windowed read has the three-stage form with no side channels. S2 through S4 are claims about languages and addresses, and no analysis argument can conjure those. They are exactly what the synthesis theorem supplies (B.8). Analysis and synthesis are halves of one proof, and the halves meet in the middle, as promised.

B.6 Independent evolution (Prop. 4.5)

Prop. 4.5 (restated). In a proper factorization, the document’s evolution decomposes into four independent timelines, one per component; in the trivial factorization, one timeline carries every change.

An application over time is a quadruple of trajectories (S(τ), q_τ, x_τ, s_τ) — x is Chapter 4’s arrange term t, renamed to stay clear of the time index τ — with doc(r, τ) = ⟦s_τ⟧(⟦x_τ⟧(⟦q_τ⟧(r, S(τ)))). Write the three stage values as v₁(r, τ) = ⟦q_τ⟧(r, S(τ)), v₂ = ⟦x_τ⟧(v₁), v₃ = ⟦s_τ⟧(v₂).

Dependency triangle. By S1 each factor is a function of its displayed arguments only, so the dependency matrix of the stage values on the four components is triangular: v₁ depends on {S, q}; v₂ on {S, q, x}; v₃ on {S, q, x, s}. Substituting s_τ → s′ leaves v₁ and v₂ identical — S2 guarantees the substitution cannot reach into another language’s meaning, S3 that the result is still an application. The same argument, one row up, for x and for q. So a change to any one component changes the document while every stage value upstream of that component is untouched: four timelines, advancing independently. Effectiveness means that each timeline can actually move the document; it is witnessed rather than proved. The witnesses are a theme that inverts colors, a layout that reverses order, a query that widens a window, and a write (delta normal form) that adds a fact inside the window. One witness each is all “independent” needs.

The fused half. In the trivial factorization there is one component; its dependency matrix is one full row; any change is a change to it. One timeline, by counting.

Corollary, cache granularity. Under S4 each vᵢ is a resource with a URI, hence with its own validator (RFC 9110 §8.8). By the triangle, vᵢ’s validator changes exactly when a component in its row changes: invalidation sets are the rows. Fused: the only resource is v₃, its row is everything, and every change invalidates the one entry there is. ∎

B.7 The homomorphism (Prop. 8.1)

Prop. 8.1 (restated). A translation φ — facts to triples, states to graphs, bindings to solution mappings — carries match, join, union, and project to SPARQL’s evaluation, clause for clause; on ground states it is a bijection.

Both sides first, then the map, then the commuting, clause by clause.

The derived side. Chapter 5’s algebra over 𝒫(Fact): a pattern P is a finite set of triples over I ∪ V ∪ Var; its evaluation is match(P)(S) = { β : Var(P) → I ∪ V | β(P) ⊆ S }; join(Ω₁, Ω₂) = { β₁ ∪ β₂ | β₁ ∈ Ω₁, β₂ ∈ Ω₂, β₁, β₂ agree where both defined }; union(Ω₁, Ω₂) = Ω₁ ∪ Ω₂; project(Ω, W) = { β|_W | β ∈ Ω }.

The deployed side. SPARQL 1.1 Query §18 defines, denotationally: basic graph pattern evaluation over a graph G as the solution mappings μ with μ(BGP) ⊆ G (§18.3, §18.5); Join as the compatible merge of solution mappings; Union as their set union; Project as restriction to the projection variables. The four defining clauses are, symbol for symbol, the four clauses above.

The map. φ sends a fact (s, p, o) to the RDF triple with s, p as IRIs and o as IRI or literal. It sends a state to the graph of its facts’ images, and a binding to the solution mapping composed with φ. On ground states φ is a bijection onto ground graphs.

The commuting. By induction on the structure of the selection term. Base: φ(match(P)(S)) = eval(BGP_{φ(P)}, φ(S)) because β(P) ⊆ S ⟺ (φ ∘ β)(φ(P)) ⊆ φ(S) — φ bijective on ground material, applied pointwise. Inductive cases: compatibility of bindings is preserved and reflected by φ (it is injective on values), so the join clauses coincide; union and project are set union and restriction on both sides, and φ commutes with both by construction. Four clauses, four checks, no remainder. ∎

Three boundaries, stated rather than buried. First, the correspondence is proved on the ground fragment; blank nodes in data re-enter through the bill for anonymity (Prop. 9.1). SPARQL’s default regime — matching blank nodes in the queried graph as constants — is skolemization, and the bill already covers it. Second, the derived algebra is the monotone core, and the correspondence covers exactly its image: the AND/UNION/SELECT fragment under set semantics (DISTINCT). SPARQL’s non-monotone extensions (OPTIONAL, MINUS) and its default multiset semantics are conveniences beyond the derived minimum, and the theorem claims nothing about them. Third, V is instantiated here as RDF’s literal terms — lexical form with datatype, identity at the character level (RDF 1.1 Concepts §3.3) — not as the values they denote: "1"^^xsd:integer and "01"^^xsd:integer are distinct terms denoting one value, and the bijection is term-level. The distinction is RDF’s own, and renamings never enter V’s elements, so the datatype IRIs riding inside literals stay opaque. The fragment is not a retreat: it is what Chapter 5 forced, found verbatim in the standard.

B.8 The synthesis theorem, with genericity exact (Thm. 8.2)

Thm. 8.2 (restated). The stack realizes the proper factorizations whose select is a term of the derived algebra and whose arrange is generic — invariant under URI renaming — and only those. The select-side condition is honest scope, not retreat: S2 grants select some language with closed semantics, not this one, and a select beyond the derived algebra — recursive, say — asks the stack for more than Chapter 5 ever derived.

Genericity, defined. Fix the reserved vocabulary V₀ ⊂ I — the form-level names the once-for-all conventions license (kind, rel, the role scheme). A renaming is a bijection ρ : I → I fixing V₀ pointwise. Renamings act on states, trees, and documents by rewriting embedded names — with one clause Chapter 6’s law forces: on a canonical tree the action is rewrite-then-recanonicalize, ρ · canon(S) = canon(ρS), because canon’s sort is an accident of spelling and carries no meaning to preserve. Without the clause even the identity transform would fail the equation below, tripped by block order alone. A transform T : Tree → Tree is generic iff for every renaming ρ and state S: T(canon(ρS)) = ρ · T(canon(S)) — the transform commutes with renaming. (The notion has a family history worth citing exactly. Genericity as invariance under domain permutations is Chandra–Harel (1980). Abiteboul and Vianu transposed it to a formal web model in 1997, and Fletcher et al. (2009) restated it for search queries. Deployed RDF practice, per Hogan’s canonicalization work (2017), renames only blank nodes and holds IRIs rigid. The definition here is the family’s missing member — IRI-renaming invariance, imposed on transforms.)

The free-theorem consequence, in Wadler’s sense — “cannot hardcode identifiers,” made exact. Say T treats u specially (u ∉ V₀) if there is a state S and a fresh u′ such that replacing u by u′ in S does not change the output by exactly the action of (u u′). If T is generic, T treats no name specially: apply the transposition ρ = (u u′), which fixes V₀, and commuting forces the output to change by exactly that action. Contrapositive: a transform that branches on the spelling of a non-reserved identifier is not generic. Data-drivenness stops being a slogan at this line.

Relative genericity — the override, bounded. Deployed arrangements are rarely generic in the strict sense, and should not be: a term that renders persons as cards must name the person class, and naming is special treatment by the definition just given. The repair is not to relax the definition but to index it. For W ⊆ I, say T is generic relative to W iff T commutes with every renaming that fixes W pointwise as well; strict genericity is the case W = ∅. The relativization is the family’s own standard allowance — Chandra–Harel’s queries are generic up to a finite set of constants — transposed like the rest. The free theorem relativizes verbatim: a transform generic relative to W treats no name outside W specially. Its special treatment is confined to a declared set, and honesty is checkable from the term’s text alone. The names it spells must lie in V₀ ∪ W. The names it does not spell it may use only opaquely — matched by equality and copied, never inspected as strings (AWWW §2.5’s opacity, now a syntactic discipline rather than a norm). Vocabulary-awareness stops being smuggling exactly when its footprint is declared.

The deployed shape of relative genericity is layering. A base term renders the canonical serialization and names no vocabulary — generic relative to ∅, and total, because canon refuses no state. Vocabulary-specific terms arrive as overrides, layered onto the base by the transformation language’s own import mechanism. Precedence is part of XSLT’s closed semantics, so S2 is undisturbed, and adding or removing an override is S3’s substitution, exercised in place. One further condition, and it does real work: an override must refine coverage, never restrict it — for every state, the layered term renders every entity the base renders, differing only where descriptions meet W. Under refinement, the failure mode of an unknown name is the base rendering rather than no rendering: every state renders; declared vocabulary renders better. (An override that seizes the root and renders only what it recognizes passes the footprint check and fails this one; both clauses are load-bearing.)

The relativization closes the smuggling question rather than reopening it, because it leaves domain knowledge exactly two doors. Through the term: named in W, bounded by relative genericity, footprint on display. Through the argument: the vocabulary travels in the state, because an ontology is facts like any other, and Chapter 17 puts it there. The term reads it from its input, and a renaming then moves description and data together, so the term stays generic relative to ∅. Term or state; footprint or argument. A transform whose behavior turns on a name found in neither is non-generic, and the free theorem catches it. There is no third place for a domain to hide.

Synthesis. Let (select, arrange, present) be any proper factorization whose select is a term of the derived algebra and whose arrange = T ∘ canon with T computable and generic — strictly, or relative to a declared W; the construction is indifferent. Realize the three factors in the deployed stack. The selection is a term of the derived algebra, hence by the homomorphism (B.7) a SPARQL term evaluating identically. canon exists and is deterministic (Prop. 6.1, RDFC-1.0 for the unnamed). T is a computable tree-to-tree function and XSLT is computationally complete on trees, so a term t with ⟦t⟧ = T exists. Genericity is preserved by writing t with no URI literals outside V₀, names otherwise held opaque. It relativizes intact: base plus declared overrides realizes the class generic relative to W, with the relativized free-theorem clause as the check that nothing was smuggled. present is a stylesheet by S2’s own requirement. S4 holds because in the deployed stack every stage value is a resource: the graph, the query result, the document each dereference (Graph Store Protocol; SPARQL protocol; HTTP). So the stack realizes the factorization — and realizes only proper ones: a non-generic arrange fails the definition just given, which is the “excluding smuggling” caveat of Chapter 8, now a clause rather than a caution.

Together with the analysis theorem (B.5): every windowed read has the form, its select window-shaped — a union of ground matches, inside the derived algebra — and the stack fills the form. This section is where the halves meet. ∎

B.9 Federation closure (17.1)

The claim. The union of two dataspace states is again dataspace-shaped: one graph per document, every document under exactly one origin, attribution intact — so federation needs no machinery beyond (5.1).

The proof. RFC 6454 computes an origin from every URI; distinct origins are therefore disjoint regions of I: o ≠ o′ ⟹ I∣o ∩ I∣o′ = ∅. A dataspace’s graph names are document URIs under its own origin (17.1), so two dataspaces’ graph families have disjoint name sets and union as families. No graph name is claimed twice, every document is still served by exactly one party, and the fourth position still carries who. On the facts, the union is (5.1) over the retyped atoms of Prop. 9.2 — merge is still set union — so federation inherits totality, order-freedom, and idempotence unchanged. Facts join exactly where names are shared (R3); nothing more is promised. ∎

One boundary, stated rather than buried: the closure is of states. A federation is not itself a dataspace — it has many origins, no single ontology — and (17.1) claims no such thing. What the parties hold before aligning and what alignment yields is Chapter 17’s price section, not this lemma.