- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
\(X\) depends on \(Y\) when what \(X\) is cannot be stated without \(Y\). For the parts of Definition 1.1 this is a matter of type: \(R\) is a subset of \(T \times T\), so the kind of object \(R\) is depends on \(T\). That \(R\) depends on \(T\), and \(T\) not on \(R\), holds by construction.
The state is the inter-block time \(s \in \mathbb {Z}\) in minutes, with set point \(10\). The feedback law is
With \(N = 3\), one contact updates the count \(c \in \mathbb {N}\) by
The shape \(\mathcal{I}_{\mathrm{Klir}}\) has two objects, the relation and the things, and one generating arrow
read “\(R\) is defined over \(T\)”. The arrow joins the parts of the definition, not two things.
Let \(T\) be a set of roles and \(P\) a set of participants. A protocol system has three layers.
(L0) Definition: a relation \(R \subseteq T \times T\).
(L1) Occupancy: an assignment \(a \colon P \to T\) of participants to roles.
(L2) Enactment: actions by participants, over time, in relation to \(R\).
A protocol is (L0). A protocol system is all three. With arrows from dependent to depended-on,
(L2) has no arrow. It is time, which the kernel holds a place for and cannot fill (Theorem 2.2).
A set \(S\) is organized when \(\exists \, a, b \in S\) with \(a \neq b\) and \(\operatorname {Bonded}(a, b)\). Two systems with disjoint compositions and at least one bond between them compose by union.
A protocol is a relation \(R\) over a set \(T\) of roles: what each role does relative to the others. This is a working definition and is not yet formalized.
A protocol system is a protocol together with participants acting in relation to it. Walch, The Fundamentals of Protocol Systems (2023), p. 5: “A protocol system is made up of a protocol, at least two people, and those people taking actions in relation to the protocol.” This is a working definition and is not yet formalized.
Put all eight shapes in one declared arrow convention and check whether Theorems 1.5 and 1.7 still hold. Then take dependency in the sense of Definition 1.2 as the weakest notion and ask whether functional dependence (Myers) and causal dependence (Joslyn) refine it. If they do, the shared arrow has one meaning, refined differently by each tradition.
Blygger replaces deletion with withdrawal and makes pins irrevocable. Model it as an instance and locate its hardness.
Bunge, Treatise on Basic Philosophy, vol. 4 (1979), Definitions 1.13 and 1.14, defines emergent properties set-theoretically. State emergence over the kernel without building the emergent structure into the model.
State machines, process calculi, temporal logics, and Petri nets can be drawn over a common skeleton. Encode a fifth formalism and test whether the skeleton survives.
Define a protocol as a relation over roles and a protocol system as an assignment of participants to those roles, and prove that every protocol system is a kernel.
Hardness can be located in a protocol by drawing its dependencies. Find a measure of hardness that compares protocols of different kinds.
Some rules create the activity they govern: there is no checkmate before the rules of chess. If a role is made by its rules, then \(T\) depends on \(R\) and the arrow reverses. Position: a role has a label, which tells the position apart, and a function, what its holder does. The label belongs to \(T\) (Walch, p. 6: a role “has a name that distinguishes it from other roles within the system”). The function is \(R\). Rules make labels into roles. A piece carved as a bishop and assigned no moves is \((T, \varnothing )\). “Moves diagonally” cannot be stated without saying what moves.
Klir places systemhood in \(R\). Walch (p. 3): “Protocol systems are always two things at once—individuals and a group.” Position: both hold, at different layers. Organization lives at (L0). The two-sidedness lives at (L1): the same participants, seen through \(a\), are individuals in roles, and seen through \(R\), are a group.
The kernel holds places for time and environment but leaves them empty. Find which time and environment content, if any, can be generated from the kernel, and state exactly what must be supplied from outside.
Does a protocol exist before anyone adopts it? Rao et al. (p. 7): a protocol that falls short “arguably … wouldn’t exist at all”. Yet they describe IPv6 as ratified in 2017 with adoption still slow (p. 16). Position: yes. \(R\) needs roles, not occupants, so what fails to get established is the protocol system, at (L1) and (L2).
For each of the definitions of Bunge, Mobus, Myers, Wymore, Mesarović, Joslyn, and Spivak, there is a functor from \(\mathcal{I}_{\mathrm{Klir}}\) to that definition’s shape that is injective on objects. With Klir’s own, the arrow sits inside all eight.
A kernel with at least one bonded pair of distinct things generates a Bunge system, and a kernel in which nothing is related to itself generates a Mobus system. Each generated system projects back to the same kernel.