The Open Ledger: Theorems 2-5 and Open Problems

Theorem 1, convergence, is machine-checked. Nothing else is. This chapter is the honest frontier: the four theorems the specification declares but no one has proven, and the open problems the specification names but does not solve. If you want to contribute mathematics to Osmol, this page is the job board.

Four theorems, still open

The statements below are quoted verbatim from spec §9, which declares them as proof obligations for the formal phase, "suggested vehicle Lean 4 or TLA+ over the small-step semantics of §6." The Theorem 1 certificate adds a third natural vehicle: continuing in Coq, where the existing proof lives. Its closing ledger also sketches the route to each; those routes are reproduced with each theorem below.

Theorem 2 (Non-interference). No delta derived from twin A's state reaches twin B unless a membrane rule of A grants it. (Security: M = 0 annihilates P; grammar forbids foreign membranes.)

Status: OPEN. Why it matters: this is the privacy guarantee. An implementer who honors it can promise a user that deny means deny: not "filtered with high probability" but "no derivation exists." Route: formalizable in the existing framework by enriching the abstract oracle back into structure, with membranes as explicit casts, so that the grant is a syntactic object the proof can case on rather than an opaque boolean.

Theorem 3 (Attention soundness). Interrupt placements at twin B never exceed B's declared budgets, for any behavior of any other twin. (Receiver sovereignty as an invariant, not a courtesy.)

Status: OPEN. Why it matters: this is O-006's promise made adversarial, that is receiver sovereignty holding against any sender strategy, not just polite ones. An implementation's interrupt classifier can only be audited against a stated invariant, and this is that invariant. Route: needs a placement layer on top of flows. The current model stops at absorption and never formalizes silent/ledger/interrupt classification, so the layer must be built before the theorem can even be stated in the proof assistant.

Theorem 4 (Granularity monotonicity). Along any flow path, granularity is non-increasing. (No composition of casts refines information.)

Status: OPEN. Why it matters: single casts going downhill is a local check (O-002); this theorem is the global closure: no composition of casts across multi-hop paths can ever reconstruct precision a membrane surrendered. Multi-twin relay is exactly where an implementer's intuition is weakest. Route: the same enrichment as Theorem 2, facts as (value, granularity) pairs, casts as lattice operations, then an induction along paths.

Theorem 5 (Spam irrationality). Under any strategy, expected return of unsolicited pressure without adopted gaps is negative. (Game-theoretic; the stake mechanism of §4.9.)

Status: OPEN. Why it matters: the anti-spam story is economic, not filter-based. stake prices unsolicited pressure instead of blocking it, and this theorem is the claim that the pricing actually works against a rational adversary. Route: game-theoretic, and the certificate is frank that it "wants a different toolbox", that is expected-utility arguments over sender strategies, not fixpoint induction. It may be the last one to fall.

One reassurance from the certificate's ledger, and it should be repeated to anyone sequencing work: none of them block Phase 3. Prototypes, the Rust core, and the wire can all proceed while these remain open: the theorems harden claims the design already makes; they do not gate the design.

Open problems

Spec §10, the specification's own honest section, names five problems that are not theorems awaiting proof but designs awaiting a designer:

  • Retraction. drop lapses a gap, but un-asserting a hold that has already equalized requires revocation-deltas, and their semantics are deferred. Monotone absorption ("nothing un-knows") is the engine of Theorem 1; retraction must be added without breaking it.
  • Conflicting holds. Two twins holding contradictory values for the same fact resolve today by provenance weight and recency. A principled belief-merge is open.
  • Truthfulness staking. Assertions carry confidence, but a staking mechanism for truthfulness (forfeit on falsification) is sketched, not specified.
  • Gap privacy. Seeking is itself revealing: registering a gap discloses what you lack. v0.2 must let membranes govern the visibility of gaps, not only holdings.
  • Lattice governance. Who defines coarse(city) per domain is a standards question, and, as the spec puts it, standards questions are political questions wearing file formats.

How to claim one

Proofs and problem-solutions enter the language the same way everything else does: as RFCs, accompanied by conformance cases. A proof RFC should state the theorem over the spec §6 semantics, name its vehicle, include the checked artifact (as osmol_convergence.v set the precedent: zero axioms, zero Admitted, Print Assumptions clean), and, where the theorem constrains implementations, contribute the conformance programs that would catch a violator dynamically. A design RFC for the open problems follows the standard template: motivation against the five axioms, precise grammar and semantics, effect on spec and suite.

See The RFC Process for the mechanics and Conformance for what a good golden case looks like. The ledger is open; the stone doesn't rush, but it does accept new carving.