The Five Axioms

Every rule in the Osmol specification derives from five axioms. This is meant literally: when a construct seems strangely strict, when a piece of syntax you expect turns out not to exist, when an error message reads more like a principle than a diagnostic, one of these five is the reason. An implementer who knows the axioms well can usually predict the rest of the language before reading it.

The axiom statements below are quoted verbatim from spec §1. The commentary after each is what the axiom costs you as an implementer: the machinery it obligates you to build, and the machinery it forbids you to build.

Axiom I. There is no send.

There is no send. No construct exists that transmits content to a party. Communication occurs only as the mesh's resolution of pressure between declared states. The sender, as a grammatical role, does not exist.

For implementers: your grammar must have no transmission production, and your toolchain must enforce that absence actively. The tombstone words (send, notify, broadcast, blast, cc, bcc, forward, reply) are reserved solely to produce O-000; the old world's verbs die loudly, not quietly. Everything that looks like delivery in a running mesh is in fact the solver resolving pressure between a hold and a seek. There is no code path in which one twin pushes content at another.

Axiom II. Programs are claims, not commands.

Programs are claims, not commands. Every statement is a declarative speech act: an assertion, a gap, a commitment, a decision, an expression, or a permission. There are no loops, no sequencing, no control flow. Order of declarations never matters.

For implementers: you are building a constraint settler, not an instruction executor. There is no program counter, no statement ordering to preserve, no evaluation order to document. Order-irrelevance is strong enough that a formatter is free to sort declarations canonically. The dissertation's osmol fmt does exactly that, because reordering cannot change meaning. If your implementation's output ever depends on the textual order of declarations (beyond the spec's deterministic tie-break on pressure, which is by (sender, receiver, fact), not by line number), you have a bug.

Axiom III. The receiver's grammar governs.

The receiver's grammar governs. Thresholds, budgets, and quiet hours are properties of the receiving twin, declared in the receiving twin's source, and no construct in any other twin's source can reference, lower, or spend them.

For implementers: attention and membrane blocks attach syntactically to the twin that owns them, and the grammar provides no way to name a foreign twin's blocks at all. This is deliberately enforced before type checking, by the shape of the syntax tree. See O-006 and O-001 for the two diagnostics that guard the property at the AST level, where tools might construct what the parser cannot.

Axiom IV. Precision only flows downhill.

Precision only flows downhill. Every value carries a granularity, and the type system admits transforms only downward along the lattice exact ⊒ coarse(g) ⊒ category ⊒ existence. Coarsening is a cast; refinement is a type error. Precision cannot be manufactured, only surrendered.

For implementers: every value in your representation carries a granularity coordinate, and every membrane transform is a cast checked against the lattice. There is no syntax for an upward cast (the grammar simply has no word for it), and an AST-level attempt is O-002. The open formal counterpart is Theorem 4 (granularity monotonicity along composed flow paths); see The Open Ledger.

Axiom V. The human lane is verbatim.

The human lane is verbatim. Expressive content crosses the mesh untransformed, unsummarized, and provenance-labeled. No transform, membrane rule, or attention rule may compress it, and no autonomous process may author it.

For implementers: express content is exempt from every transform in your pipeline. A membrane or attention rule whose selector matches an expression is O-004; an expression authored by an autonomous process is O-005. Quiet hours may queue an expression; nothing may summarize or silence one. Provenance (human by default, assisted permitted, autonomous unrepresentable) travels with the content.

A table of consequences

Each axiom appears three times in the language: as a principle, as a grammar feature, and as a diagnostic. Reading across a row is the fastest way to see that the errors are the ethics.

Axiom II is the only row without a diagnostic, and that too is a consequence: a property that holds because the grammar has no way to violate it needs no error message. The full catalog of impossible sentences lives in What Cannot Be Written.

The Speech-Act Type System

Where conventional languages type data (int, string), Osmol types acts. Every top-level statement inhabits exactly one of five kinds, and the kind determines how the equilibrium engine treats it. This section is spec §3; treat it as the map of the whole constructs reference.

Assertion (hold): a claim that the twin possesses a value, with optional uncertainty, confidence, and decay. Assertions are the mesh's supply side.

Gap (seek): a first-class record of absence, meaning the twin lacks a value and registers standing interest. Gaps are the demand side, and the only thing that can attract flow. A gap may carry a deadline and an escalation policy.

Commitment (owe): a promise from this twin to a party, with a due instant. Commitments generate structural gaps automatically: an unmet owe implies the counterparty's seek for its status.

Decision (decide): an open choice among enumerated options with a deadline. Decisions are gap generators (one gap per option's unevaluated consequences) and emit an assertion upon resolution.

Expression (express): human-lane verbatim content directed to a party, carrying mandatory authorship provenance (human by default; assisted permitted; autonomous unrepresentable, see O-005).

Two auxiliary families complete the system. Permissions: membrane, whose rules are typed as granularity casts guarded by conditions. Postures: attention, bond, role, and stake, which parameterize the pressure function rather than the state.

Values are typed as quantity, instant, place, enum, or entity, each carrying a granularity coordinate. The full type of an assertion is therefore a triple: (value type, granularity, temporal validity), for example:

place @ exact, decays 20:00

read as: a place-typed value, at exact granularity, valid until 20:00. All three coordinates matter to the engine. The value type drives relevance matching between holds and seeks; the granularity coordinate is what membrane casts operate on (granularity); and temporal validity feeds the urgency term of the pressure function (pressure).

If you carry only one thing from this page into an implementation, let it be this: the five kinds are not statement categories for documentation purposes. They are the type system. Each kind has a distinct role in the engine (supply, demand, structural demand, demand-generation-plus-eventual-supply, and the protected verbatim lane), and every downstream rule in the language (what flows, what casts, what may never be touched) dispatches on that kind first.