Protocols are systems

Questions

From the symposium talk (September 24, 2026), the SIGFPT session (October 2, 2026), and replies to the note (October 7, 2026).

Is a protocol just the rules?

Yes. Rules are relations, and in Klir’s definition the relation is where systemhood resides. A protocol defined over its participants forms a system.

See Chapter 3 of the blueprint. A protocol is a relation defined over a set of roles. Participants assigned to those roles, acting over time, form what Walch calls a protocol system.

Isn’t Klir’s relation more fundamental than a dependency?

It is, and the shared arrow already says so. The arrow is not inside the relation. It runs from the relation to the things it is defined over.

Klir’s relation may be directed, like an ordering, or symmetric, like a partition. The arrow every definition shares is one level up: a relation cannot be stated without its things. That arrow is the shape of Klir’s own definition, and it is the shape that embeds, by position, into all eight. See Chapter 1 of the blueprint.

Isn’t that dependency true by construction?

Yes. It is not a result. It is what Klir’s definition says when read aloud.

(R) is a subset of (T \times T), so the kind of object (R) is depends on (T). That is the definition of dependency used here (Chapter 1). The results are elsewhere: the arrow sits in all eight definitions, and at the level of asserted arrows nothing larger is shared.

Shouldn’t Klir’s shape have two arrows, one for each end of a pair?

For the data, yes. The one-arrow shape records dependency, and the two-arrow shape is not shared.

Each element of (R) is a pair with a first and a second thing, so (R) maps to (T) twice, (R \rightrightarrows T). Read as a schema for data, that is the shape of a graph. Collapsing both arrows to one forgets how (R) refers to (T) and keeps only that it does. The two-arrow shape does not fit every definition: Myers’s shape has at most one arrow between any two positions.

Is “dependency” the same thing in every tradition?

Not shown. The embeddings place the arrow by position, not by meaning.

Into Myers the arrow lands on the map by which state determines output, a functional dependence. Into Joslyn it lands on the effector acting on the controlled variables, a causal one. The shape files also declare different arrow conventions. Putting all eight in one convention, and asking whether functional and causal dependence refine the weakest notion, is an open problem.

Can arrows go both ways, directly or through something in between?

Among things, yes: a relation may run both ways. Among the parts of a definition, the shared floor is one arrow in one direction.

Details

Each definition has parts, such as Joslyn’s controller, effector, and controlled variable, or Willems’s time, signal, and behavior. A way back between two parts, direct or through a third, means following one arrow and then another. Willems’s definition, as encoded, never has two arrows in a row (no_two_chain), so no way back fits inside it, and the floor shared by every definition stays one arrow (connected_is_single_arrow).

Two-way dependency between parts does appear in individual definitions. Joslyn’s encoded shape has one: the effector acts on the controlled variable, and the controlled variable feeds back to the effector. It is not shared by every definition. This is a result about the definitions as encoded. Willems’s interconnection layer, for one, is not encoded yet.

Rosen marks an outer edge. His 1978 definition relates states by whether every observable agrees on them, a relation that always runs both ways. A kernel whose relation has some pair without its converse has no Rosen view at all (rosen_no_view_of_asymmetric, ViewGeneration.lean).

Can time and environment be built from the primitive?

The core can hold places for time and environment, but it cannot fill them.

Derived from the core alone? No. When the kernel generates a richer view, the time and environment slots come out empty, and the generated energy view is provably static. Real time and real environment are content supplied from outside.

Represented as parts of a definition? Yes. Willems encodes time as a part that behavior depends on (indexed_by, ShapeWillems.lean). Bunge and Mobus each give environment its own part of the definition, the E in their tuples.

Details

ViewGeneration.lean generates each tradition’s view from the kernel: the things, the relation, and the arrow between them. Each generated view projects back to the same kernel, and distinct kernels give distinct views. Each view has a price:

The generated views fill environment, external flows, boundary, history, and timescale with empty or trivial values. Spivak’s energy-driven view always exists but is provably static (Kernel.toSpivak_static, SpivakSystem.lean), so motion needs value data from outside the kernel. Generating non-trivial time and environment content is open.

Where do dynamics enter?

Not at the floor. Relational structure alone is static. Bunge’s mechanism and Mobus’s transformations, history, and timescale carry the dynamics.

The kernel’s generated energy view is provably static (Kernel.toSpivak_static). Bunge’s mechanism (the M in his system tuple) and Mobus’s transformation, history (H), and timescale (Δt) are where change enters.

What about emergence?

Not yet engaged here. Bunge gives a set-theoretic definition.

Bunge, Treatise on Basic Philosophy, vol. 4 (1979), chapter 1, Definitions 1.13 and 1.14: the properties a thing gains over an interval are emergent relative to it, and absolutely emergent if no thing had them before. Whether the core can state emergence without building it in is open.

On reading arrows as time

Here an arrow means “depends on,” not “comes before.”

Read as temporal links, two-way arrows raise hard questions of causality and simultaneity. ShapeWillems.lean states the convention as “dep_on is predication, not causation.” Time is a separate part (Mobus’s history and timescale).

Where to start with Lean?

Read Challenge.lean. It states every claim without the proofs.

Each headline claim appears there with its full type, so a reader can check the result without reading the proofs. For learning Lean: Mathematics in Lean. Reading one statement, the hand-washing theorem:

theorem handwashing_contamination_bounded (n c : ℕ)
    (hsafe : c ≤ sanitizePeriod) :
    contaminationStep^[n] c ≤ sanitizePeriod
Piece Meaning
(n c : ℕ) for any whole numbers \(n\), the steps taken, and \(c\), the starting count
(hsafe : c ≤ sanitizePeriod) assumption: \(c \le N\)
contaminationStep^[n] c \(f^{n}(c)\), one step applied \(n\) times
≤ sanitizePeriod conclusion: \(\le N\)

Lean rejects the file unless the proof that follows checks every step.

Pointers from the sessions, not yet engaged