The Granularity Lattice

Every value in Osmol carries a second coordinate alongside its content: how sharp it is. Axiom IV (precision only flows downhill) turns that coordinate into a one-way street, and this chapter is the map of that street.

The lattice

exact ⊒ coarse(g) ⊒ category ⊒ existence

exact         19:40 ±5m                     the value as held
  │ cast
  ▼
coarse(g)     ~19:40, to the half hour      rounded to a declared grain
  │ cast
  ▼
category      "evening"                     only the class of the answer
  │ cast
  ▼
existence     an ETA exists                 only that a value exists

Four rungs. exact is the value as held. coarse(g) is the value rounded to a declared grain: coarse(30m), coarse(city), coarse(week). category keeps only the class of the answer. existence says only that a value exists at all. Every value type (quantity, instant, place, enum, entity) carries a granularity coordinate, and the full type of an assertion is the triple (value type, granularity, temporal validity).

Movement down the lattice is a cast: legal anywhere, meaning-preserving in the only direction that can be honest. Movement up is a type error, because refinement would mean manufacturing information the source never surrendered. The grammar cooperates by having no word for it (the membrane transform vocabulary contains only the four rungs and deny), and the checker backstops it with O-002: precision cannot be manufactured, only surrendered.

Casts in flight

Membrane transforms are the cast mechanism: each flow crosses the sender's membrane and is cast to the rule's grain on the way through. The cast also prices the flow. Inside P = R × U × T × M − C, the factor M is the cast weight: exact 1.0, coarse(g) 0.7, category 0.5, existence 0.3, deny 0. Coarser knowledge exerts less pressure, which is exactly right: a city-grain location rarely justifies interrupting anyone.

The v0.1 interpreter renders casts textually in apply_cast: exact passes the value through unchanged; coarse renders ~value [coarse(30m)]; category renders value [class-level]; existence renders [exists]. You can see two of these in the real dinner trace:

t2  maya.eta(dinner) --exact--> raj   P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3   [silent]
t3  maya.status(atlas.review) --category--> raj   P=0.65 (R1.0*U1.3*T1.0*M0.5) > theta[family]=0.3   [silent]

After t2, raj's twin holds 19:40 ±5m, exact, because raj is family. After t3 it holds in-progress [class-level], that is the review's status at category grain, with M = 0.5 visibly discounting the pressure. And if raj were not bonded trust high by maya, her second membrane rule (eta(*) -> others: coarse(30m)) would match instead, and his twin would absorb ~19:40 ±5m [coarse(30m)]: the same fact, honestly blurred.

What is not yet proven

Theorem 4 (granularity monotonicity) states that along any flow path, granularity is non-increasing: no composition of casts refines information, even across multi-hop flows through several membranes. It is stated in spec §9 and it is open. The Theorem 1 machine-check (the certificate) abstracts membranes into a boolean oracle, so it says nothing about grains; enriching the oracle back into explicit casts, with facts as (value, granularity) pairs, is the identified route to formalizing Theorems 2 and 4 in the same framework; see the open theorems.

Honesty about v0.1, likewise: the reference interpreter does not track granularity coordinates on holdings. Values are uninterpreted strings, and the cast markers above are renderings, not typed grains. So O-002 cannot yet fire mechanically; nothing in the engine knows that coarse(city) is below exact. A conforming implementation that types the lattice for real would be a major, welcome step past the reference.

Who defines coarse(city)?

The lattice's shape is fixed by the spec. Its grains are not: what counts as coarse(city) for a location, coarse(week) for a date, coarse(band) for a salary, differs by domain and by jurisdiction, and spec §10 is plain about what that means: who defines a grain per domain is a standards question, and standards questions are political questions wearing file formats.

The planned venue for those politics is the Lattice Registry, the governance-flavored appendix of the documentation site sketched in the engineering dissertation (Ch. 9). It defines standard granularity lattices per domain, so that two independent implementations coarsen the same value the same way. It does not exist yet. If you have a domain whose grains you understand (logistics, medicine, payroll), a registry entry is a good first RFC: it is small and concrete, and everyone who comes after will build on it.