What is proved (§4.3–4.4)

Theorem 64 — preservation

The registry stays well-formed: parent pointers land in it; provisions pairwise disjoint; every installed fiber's ω is total on d and names installed fibers. The L-Unload guard is what carries the last clause; a corollary is that a removed name can be safely reissued.

In words: the bookkeeping never gets corrupted — no dangling parent, never two providers of one key, and no fiber ever holds a committed view pointing at a fiber that has gone.

Lemma 66 + Theorem 68 — temporal composability, global form (recovery exactness)

Every run is pairwise independent — because every coeffect carries a commutativity witness and non-entangled pairs meet Thm 47; entangled pairs (provider/consumer at a shared key) are handled by Lemma 67: the rules never interleave them in the order that would separate them. Then: applying n's accumulator at any point in its episode leaves every table where the other fibers' steps alone would have left it from the episode's start. Running an inverse withdraws that fiber's contribution and nothing else. Cor 69: at episode end the fiber's table is empty — the premise O-Remove needs.

In words: disabling a plugin removes exactly what that plugin added and nothing else, no matter what other plugins did before, during, or after — and it leaves the plugin's own table empty, so it can be removed.

Theorems 70–71 — spatial composability, global form

Ordering (70): a fiber begins only when its dependencies are provided; if m committed key k to n, then n's episode strictly contains m's, and σₙ(k) moves only by declared operations. Resolution coherence (71): a transition runs against one resolution throughout; if the target moves the fiber Diverts and Cor 69 cleans up. No transition straddles two resolutions.

In words: a plugin never starts before its dependencies are up; a provider outlives every consumer that got a key from it; and a plugin caught half-loaded when a dependency changes is backed out, not finished against the wrong dependency.

Theorem 73 — progress

Given ≺ (n ≺ m ≔ pₙ ∩ dₘ ≠ ∅) acyclic, iterator length bounded, finitely many names: no deadlock (some rule applies whenever not quiescent) and termination (S(n) ≤ (K+3)(V(n)+1); each turn of a target is paid for by a step of a ≺-smaller fiber). Every maximal lifecycle run ends quiescent.

In words: the system never gets stuck waiting on itself, and it settles in a bounded number of steps — provided no plugin needs a key that it (directly or through others) provides itself, which is the one thing you must check.

Theorem 80 — confluence (the headline)

Under totality on provision (a finishing activation installs all of p, Def 76): the quiescent state is the one reached by the same orchestration steps followed by one episode per supported fiber, in dependency order, never unloading. "Dynamic history leaves no trace." Two runs with the same inputs agree up to ≃ and renaming. Machinery: the support set A (Def 74 — not retired, parent supported, every declared key provided by a supported fiber; well-founded, and equal to the Active set at quiescence, Lemmas 75, 77), transposition of adjacent independent steps (Lemma 78, trace-theory style), deletion of closing episodes (Lemma 79).

In words: however the system got to where it is — plugins added, removed, swapped, re-enabled in any order — once it settles it is exactly where a clean start with the same final configuration would have put it. History leaves no trace.

Licenses: reason about a Cordis app as if statically assembled; a loader may reconcile incrementally and land where a from-scratch load would. Delimits: it speaks of state, not of emissions along the way (§6.1); FAILED fibers are excluded, since whether an iteration raises depends on the state it met.