Equilibrium and the Small-Step Relation

This chapter is the formal heart of the book: what an Osmol program is once the parser is done with it, how the mesh moves, and why it always stops. If you are implementing a solver, everything you must preserve is on this page; everything you may vary is not.

Deployment, not execution

An Osmol program does not run. Per spec §6, it is deployed: the compiler emits three artifacts, a typed state schema for the on-device model, a membrane policy set installed into the participant's edge membrane object, and gradient triggers registered with the mesh. Source never executes; it is not even present at runtime. What evaluates is the mesh, continuously and event-driven, over the deployed state of every participant.

This is the deepest consequence of Axiom II. Because programs are claims rather than commands, there is no program counter, no call stack, no "current line." The only dynamics the language has are the dynamics of pressure between declared states. So the semantics is small enough to fit in one rule.

The small-step relation

The mesh evaluates the pressure function P = R × U × T × M − C over every linked pair where A holds k and B seeks g. A flow fires iff P > θ_B(A). When it fires, it synthesizes an understanding-delta δ (the minimal signed assertion, cast to the membrane's granularity) and B absorbs it. The spec §6 gives the step rule:

⟨S_A, S_B⟩  ──[ P > θ_B ]──▶  ⟨S_A, S_B ⊕ δ⟩      where gap(g) ∉ S_B ⊕ δ

Read the side condition carefully: absorbing δ closes the gap. The closing is the definition of a step, not an optimization. Also note what the rule does not touch: S_A appears unchanged on the right. Flows are not transfers; A loses nothing, and B's state only grows.

Absorption is monotone: deltas only close gaps and add assertions; nothing un-knows. Transforms are monotone too, but downward: every membrane cast moves a value down the granularity lattice, never up (Axiom IV). Two monotone directions, one for knowledge and one for precision, and no rule in the system violates either.

The Datalog family

Monotonicity is not a style choice. It is what buys termination. A finite fact base evolving under monotone rules is exactly the setting of Datalog, and it inherits Datalog's central theorem: evaluation reaches a least fixpoint in finitely many steps. The spec names that fixpoint equilibrium, and calls it the halting state of every Osmol mesh between external events.

The argument, in short: the mesh starts with finitely many gaps; every step closes exactly one and creates none; therefore no run of the step relation can be longer than the initial gap count. Equilibrium is the state where no pressure clears any threshold, either because every gap is closed, or because what remains open is priced above what any sender's standing can reach. Both are stable. Both are success. A mesh with no gaps at all admits no step whatsoever: silence is a fixpoint.

External events (a new declaration, a decay firing, a human judgment injected into a decide, legacy email arriving through the adapter) perturb the state, and the solver settles again. The life of the mesh is therefore a sequence of settlements punctuated by the world. The spec has a line we should keep whole: "Communication, in this model, is what settling looks like from the inside."

The full formal treatment, with the machine-checked proof, is in Theorem 1.

Placement

Settlement decides what B now knows; placement decides what B's owner sees. Each absorbed delta is classified into one of three placements (spec §6):

• silent: the state updates; nothing renders. This is the majority case: the participant simply possesses current knowledge on next reference.
• ledger: the delta surfaces on the consequence-sorted board of commitments, decisions, and open questions, without interruption.
• interrupt: the delta renders now, debiting the sender-class budget declared in the receiver's attention block.

Expressions bypass classification entirely into the human lane, subject only to quiet, the one channel that placement may delay but never touch (O-004).

The Osmosis Protocol spec (§6) specifies the fuller mechanics this classification grows into: interruption budgets denominated per link and per period, chronic overdraft raising the effective θ for that sender, and interruption-class deltas required to carry a declared consequence-if-ignored field verified for plausibility. That machinery is protocol-future: the language reserves its place; v0.1 implements the three-way classification only (see the pragmas).

The solver shape

The step relation says what a step is; it deliberately does not say how to find one. The engineering dissertation (Chapter 3) fixes the reference shape: the solver is event-driven with a fixpoint sweep. Any state change at either end of a link enqueues gradient evaluation; the loop then fires the maximal-pressure flow, applies the membrane cast, absorbs, and repeats until no pressure clears any threshold. Among fireable flows of equal pressure, order lexicographically by (sender, receiver, fact); this is the determinism rule that makes golden traces possible across implementations.

Decays and deadlines enter as a monotone clock parameter: the clock perturbs urgency, and each perturbation may allow new settling, but between perturbations the convergence argument is untouched, because the clock never un-closes a gap. This is why "event-driven" is safe: there is no schedule the solver could choose, no interleaving it could pick, that breaks termination. Fire any fireable flow in any order and the mesh still finds the floor; fire the maximal one in tie-broken order and every implementation finds the same floor, step for step.

That is the entire contract a solver must honor: monotone absorption, downward casts, receiver-owned thresholds, maximal-pressure selection with the lexicographic tie-break, and the runtime assertion that flows never exceed the initial gap count. Everything else (data structures, scheduling, habitat) is yours.

Why the loop must terminate is no longer an argument in prose. It is a theorem, checked by a machine that cannot be persuaded. The next chapter is its certificate: Theorem 1.