ora-0153

13.2 Safety under a changing information shape

Online deployment changes the information category. New agents appear, a shared cache becomes visible, an unplanned channel is discovered, or a tool creates a delayed process that outlives its initiating decision. Write \(i:\mathbb I_0\to \mathbb I_1\) for the passage from a declared information shape to a richer realized shape. Extending a safe policy from \(\mathbb I_0\) to \(\mathbb I_1\) is then a Kan-extension problem.

Theorem 13.3 Safety transport by pointwise right Kan extension

Let \(j:\mathcal S\hookrightarrow \mathcal E\) be a replete full subcategory, let \(P:\mathbb I_0\to \mathcal S\), and suppose \(\operatorname {Ran}_i(jP)\) exists pointwise. If \(\mathcal S\) contains the limits in \(\mathcal E\) of all diagrams indexed by the comma categories \((b\downarrow i)\), for \(b\in \mathbb I_1\), then the canonical extension \(\operatorname {Ran}_i(jP)\) factors through \(\mathcal S\).

Proof

The pointwise formula is

\[ (\operatorname {Ran}_i(jP))(b) \cong \lim _{(b\downarrow i)}jP. \]

By hypothesis each such limit is an object of the replete subcategory \(\mathcal S\). Functoriality of pointwise right Kan extension supplies the transition maps, and fullness of \(j\) places those maps in \(\mathcal S\). Thus the entire extension factors through \(j\).

This theorem says exactly what an appeal to universal extension does not say by itself. Safety transports only when the admitted execution subcategory is closed under the limits used to infer behavior at the new information sites. If an unexpected communication channel changes the comma categories, or if their limits leave \(\mathcal S\), a proof for the declared isolation shape does not apply to the realized deployment. The resulting failure is a declaration defect before it is an optimization defect.