Protocols are systems

A protocol is a relation over roles, so a protocol is where a system's systemhood lives.

Note|Blueprint|PDF|Dependency graph|Lean source|Questions|Talk

Klir defines a system as a set of things \(T\) and a relation \(R \subseteq T \times T\). The relation cannot be stated without the things, and that dependence sits in the same position in all eight definitions encoded here. Whether it means the same thing in each is open. A protocol is rules, and rules are relations, so a protocol is the part of a system where systemhood resides. This project states that claim precisely, proves what can be proved in Lean, and keeps the rest as open problems.

30 statements · 16 formalized in Lean · 10 open problems

Contents

• Note. Relations, components, and the shared arrow, an answer to a SIGFPT question on relation and dependency, with three definitions of protocol set against it.
• Blueprint. Definitions, theorems, and open problems, each linked to its Lean declaration. Also as a PDF.
• Dependency graph. What is proved, what is stated, and what is open.
• Questions. Questions raised at Protocol Symposium 2026 and at SIGFPT, with short answers.
• Talk. Protocols are Systems, Protocol Symposium 2026, September 24, 2026.

Contributing

Discussion takes place in SIGFPT, the formal protocol theory group of the Protocol Institute. Issues and pull requests are welcome on GitHub. The open problems in the blueprint are the natural places to start.

Building

lake exe cache get && lake build

The Lean files depend on systems-science-foundations, pinned in lakefile.lean. The blueprint is built with leanblueprint.

Changelog

• 2026-10-07. The note. Dependency defined; the arrow’s meaning across definitions stated as open; protocol layers and three open problems in Chapter 3.
• 2026-10-05. Blueprint and dependency graph. The shared arrow is stated between the parts of a definition, \(R \to T\), not between things.
• 2026-10-02. Companion page for the SIGFPT session.
• 2026-09-24. Talk at Protocol Symposium 2026.

How to cite

Thornton, S. (2026). Protocols are systems. Halcyonic Systems. halcyonic.systems/protocols-are-systems