Theorem 1, Convergence, Machine-Checked

The claim

Spec §9 states it in one sentence:

Theorem 1 (Convergence). Every finite mesh with no external input reaches equilibrium in finitely many steps.

This is the theorem the whole design leans on. A language whose runtime is "keep flowing until nothing flows" is only a language if the flowing stops. For Osmol it does. And unlike Theorems 2-5, which remain open obligations, this one is no longer a claim. It is machine-checked.

What the machine certifies

The proof lives in osmol_convergence.v, checked by Coq 8.18.0, accepted on the first compile. Three statements are certified:

  • convergence: the osmosis step relation is well-founded, so there exists no infinite sequence of flows. Every finite mesh, left without external input, settles. Equilibrium is not a hope of the design but a mathematical necessity of it.
  • chain_bound: the quantitative version. A mesh whose twins carry g open gaps in total reaches equilibrium in at most g flows. So settling is bounded by the amount of unmet demand, and by nothing else.
  • zero_is_equilibrium: a mesh with no open gaps admits no flow at all. Silence is a fixpoint, not a failure. A quiet phone is the system working.

The file ends with Print Assumptions on all three theorems, and Coq's answer is Closed under the global context: zero axioms, zero Admitted. The verifier itself reports that nothing was assumed.

The model, and the honesty block

Machine-checked does not mean the whole language is proven, and this section is the mandatory fine print. The .v file carries its own honesty block in its header; here is what it says, restated without softening.

A twin, in the model, is a pair (holds, gaps): the assertions it possesses and the absences it seeks. That is all. Membrane, trust, urgency, and threshold are folded into a single boolean oracle allowed a b k, read as "the membrane grants a→b on k, and the pressure clears b's threshold." The theorem is then quantified over all oracles: convergence is proven for every possible membrane policy, pressure formula, and attention budget at once, including adversarial ones. This is a strengthening, not a cheat: a property that holds for every oracle certainly holds for the one your implementation computes.

But it means, equally, that the proof is over the flow bookkeeping, not the pressure arithmetic. Nothing in the certificate checks that P = R × U × T × M − C is computed correctly, that thresholds are compared correctly, or that membranes cast correctly. What is checked is the skeleton those computations hang from: a flow requires a holder, a seeker, and a grant; its sole effect is to close one gap and add one holding; no rule creates a gap.

Finally, the theorem's own precondition, "no external input", is encoded structurally: the step rule is the only rule in the system. A real mesh is perturbed continuously by new declarations, decays, and (someday) arriving legacy email. What the theorem guarantees is that between perturbations, the solver always finds the floor. It never oscillates and never runs away.

A guided read of osmol_convergence.v

The file is under a hundred lines of actual proof, and you can read it in full in one sitting. The tour:

The universe. fact is nat (facts drawn from a countable universe, without loss of generality), with decidable equality (fact_eq_dec).

The records. twin is { holds : list fact ; gaps : list fact }. mesh is a list of twins plus the oracle: allowed : nat -> nat -> fact -> bool, indexing sender and receiver by position.

The measure. total sums gap-list lengths across twins; gapcount m is the mesh's total open demand. This single number is the proof's fuel gauge.

The step. One inductive, one constructor:

Inductive step : mesh -> mesh -> Prop :=
| flow : forall (m : mesh) (a b : nat) (A B : twin) (k : fact),
    nth_error (twins m) a = Some A ->
    nth_error (twins m) b = Some B ->
    In k (holds A) ->
    In k (gaps B) ->
    allowed m a b k = true ->
    step m (Mesh (replace (twins m) b
                    (Twin (k :: holds B)
                          (remove fact_eq_dec k (gaps B))))
                 (allowed m)).

Twin a holds k, twin b seeks k, the oracle grants it; the effect at b is that gap k closes and holding k appears. Nothing else moves. This is spec §6's monotone absorption, and the absence of any second constructor is "no external input."

Two lemmas of list surgery. remove_lt: removing a fact that is present strictly shortens the list, so absorption really closes something. total_replace_lt: replacing one twin with a twin of strictly fewer gaps strictly lowers the mesh total.

The heart. step_decreases : step m m' -> gapcount m' < gapcount m. Every flow strictly reduces total open demand. Notice what this lemma is: the axiom the language was built on (absorption is monotone; deltas only close gaps), now arriving as the engine of the proof. The spec's promise and the proof's engine are the same sentence.

The theorems. convergence is well_founded (fun m' m => step m m'), obtained by mapping meshes into ℕ via gapcount (well_founded_lt_compat): no infinite descending chain of flows can exist because no infinite descending chain of naturals does. chain_bound inducts over any chain of n flows to get n <= gapcount m. zero_is_equilibrium inverts a hypothetical step out of a zero-gap mesh into a contradiction: the seeker's gap list must be simultaneously empty and inhabited.

The sanity demo. The file closes with the maya/raj mesh from spec §8, distilled: fact 1 stands for eta(dinner); maya = Twin [1] [] holds it, raj = Twin [] [1] seeks it, the oracle says yes to everything. Checked examples: gapcount m0 = 1, a flow exists, and by chain_bound, equilibrium in at most one flow.

The audit. Three Print Assumptions commands: trust, but verify the verifier.

Reproduce it yourself

From the certificate, verbatim:

apt-get install coq        # Coq 8.18+
coqc osmol_convergence.v   # exit code 0; prints the assumption audit

The proof is not a PDF that asks for your confidence. It is a program whose type checker cannot be persuaded, and you can run it on the bus.

The runtime shadow of the proof

Theorem 1 has one more life: as an assertion in every implementation. The reference interpreter's settle loop carries it inline:

assert flows <= g0, "Theorem 1 violated — impossible"

where g0 is the initial gapcount, and every trace prints the bound and its verdict (EQUILIBRIUM after 3 flows (Theorem 1 bound 3: respected)). The engineering dissertation makes this a non-negotiable of the core, in every habitat: the proof guarantees the assertion cannot trip; "shipping the assertion anyway is how an implementation confesses instantly" if it ever betrays the semantics. A solver that trips it has not found a bug in the mathematics. It has proven, at runtime, that it is not implementing Osmol, which is precisely the kind of self-incrimination a conformance-governed language wants built in.

  • Equilibrium: the semantic model the proof distills.
  • Open Theorems: Theorems 2-5, honestly labeled as open.
  • Conformance: how the bound becomes a dynamic test on random meshes.