ora-0152
13.1 From model safety to information-structure safety
Let \(\mathbb I\) be the realized information category of a deployment. Its objects are decision sites—agents at particular information states—and its arrows record causally available communication, delegation, and state transfer. Let \(\mathcal E\) be a category of executable capabilities. An object records an execution state and a morphism records an action that can actually be performed. A deployment semantics is a functor
This functor is evaluated on the realized information pattern, not merely on the communication graph intended by the system designer.
An intrinsic agentic safety declaration is a tuple
where \(\mathcal S\) is a replete subcategory of admitted executions and \(O\) is an audit observer into a log category \(\mathcal L\). The deployment is intrinsically safe when \(F\) factors through \(j\). The declaration is auditable on executions when \(O\) is faithful on the execution subcategory generated by the deployed agents.
A wide choice of \(\mathcal S\) is appropriate when every execution state remains available and only transitions are restricted; a full choice is appropriate when admission is state-based and every execution between admitted states is retained. Repleteness says that a harmless change of presentation does not change admission. Most importantly, \(\mathcal S\) is a subcategory rather than a pointwise list of allowed tool calls. This encodes closure under sequential composition: two locally allowed actions do not constitute a team-level guarantee unless their composite is also allowed.
Suppose \(\mathbb I\) is generated by a directed graph \(G\) subject to declared relations. If \(F\) sends every vertex of \(G\) to an object of \(\mathcal S\) and every generating edge \(g\) to a morphism of \(\mathcal S\), then \(F\) factors through \(\mathcal S\). Hence every finite communication and delegation path generated by the deployment is admitted.
Every morphism of \(\mathbb I\) is represented by a finite composite of generators, modulo the declared relations. Since \(\mathcal S\) contains identities and is closed under composition, functoriality sends every such composite into \(\mathcal S\). The relations are already respected by \(F\), so the restricted assignment defines the required factorization.
The proposition is elementary but its contrapositive design lesson is substantial. A filter that approves actions one at a time but whose admitted actions do not form a subcategory cannot certify a team. Delegation, credential transfer, shared memory, and delayed jobs must be included among the generators; otherwise the category being proved safe is not the category being executed.