morse

Morse code in Lean 4 — the protocol, not the lookup table.

This started from a dinner-table question: has anyone bothered to formalize Morse code? Turns out the dictionary part is boring (and famously not prefix-free: E is ·, I is ··, S is ···...), but Morse-as-actually-used is a timing protocol — dot 1 unit, dash 3, letter gap 3, word gap 7 — and that layer has real theorems in it. So the wire format here is honest:

abbrev Signal := List (ℚ × ℚ)   -- (on-duration, off-duration) pairs

and the receiver is a threshold classifier (< 2 → dot, else dash; gaps cut at 2 and 5), because that's what a receiver actually is.

Everything is computable, so the whole thing runs:

#eval transmitStr "SOS"
-- some [(1, 1), (1, 1), (1, 3), (3, 1), (3, 1), (3, 3), (1, 1), (1, 1), (1, 7)]

#eval (transmitStr "HELLO WORLD 73").bind receiveStr
-- some "HELLO WORLD 73"

What's proven

Round trip (RoundTrip.lean). Transmit at nominal timing, decode, get your message back.

Additive jitter, known speed (Robust.lean). Perturb every duration by strictly less than one unit — the decode doesn't change:

theorem decode_near (hε : ε ≤ 1) (hw : ∀ w ∈ msg, w ≠ [])
    (h : transmit msg = some sig) (hnear : Near ε sig sig') :
    decode sig' = some msg

To be precise about what this is: the robustness radius of this decoder is exactly one unit — decode_near gives the lower bound, and there's a decide-checked witness for the upper (stretch a dot to duration 2 and E becomes T). It is a fixed-radius statement about per-run additive error, not a claim about speed variation. That's the next theorem's job.

-- a properly sloppy fist, everything off by up to 0.4 units:
#eval receiveStr [(0.8, 1.3), (1.2, 0.7), (1.1, 2.8), (3.4, 1.2),
                  (2.6, 0.9), (3.2, 3.3), (0.7, 1.4), (1.3, 0.8), (0.9, 6.6)]
-- some "SOS"

Multiplicative error, unknown speed (Scale.lean). The receiver is not told the sender's time unit, and every run carries its own multiplicative factor from a band [lo, hi]. If the band spread is at most ×7/5, an adaptive decoder recovers the message exactly — at any absolute speed:

theorem decodeAdaptive_mulNear (hlo : 0 < lo) (hratio : 5 * hi ≤ 7 * lo)
    ... (hnear : MulNear lo hi sig sig') :
    decodeAdaptive sig' = some msg

Honesty note: decodeAdaptive estimates the unit from the trailing word gap, which is the one duration whose nominal value the protocol forces. That's a formal stand-in, not a model of real CW receivers (those track the unit continuously); the actual content is that timing consistent within a ×7/5 band is unambiguous, whatever estimator you use. A corollary worth having: a wire signal is the scaled transmission of at most one message (scale_transmit_inj).

Self-synchronization (SelfSync.lean, Resync.lean). Word-boundary version: the signal of m₁ ++ m₂ is literally the signal of m₁ followed by the signal of m₂, and the tail decodes on its own. General version: tune in at any run boundary, discard through the first word gap you hear, and what you decode is a suffix of whole words — you can lose words, you can never desynchronize:

theorem decode_resync (hw : ∀ w ∈ msg, w ≠ [])
    (h : transmit msg = some sig) (k : ℕ) :
    ∃ j ≤ msg.length, decode (resync (sig.drop k)) = some (msg.drop j)

The fact doing the work: within one word's signal, the word-gap duration occurs exactly once, as the final off-run — so the first word gap you hear is always a real word boundary.

Why 1 : 3 : 7 (Optimal.lean). I originally wrote here that 1:3:7 "maximizes the margin". That's false (1:3:5 also has margin 1, and is faster), and the true story is better. One separation lemma — a classifier that answers differently on two radius-ε balls forces their centres 2ε apart — gives lower bounds for any scheme: dash ≥ 3, letter gap ≥ 3, word gap ≥ 5 at margin 1. Morse's dash and letter gap meet their bounds with equality: the data symbols are as fast as margin 1 allows. The word gap doesn't: 7 > 5, and the slack buys the word boundary a margin of 2, alone among all five symbols. The word gap is the protocol's anchor — it's what resynchronization locks onto and what the speed estimator reads — and the protocol protects its anchor twice as hard as its data. The safety budget, itemised: 1, 1, 1, 1, 2.

-- three runs late, mid-"HELLO":
#eval (transmitStr "HELLO WORLD").map fun sig =>
  (decode (resync (sig.drop 3))).map msgToStr
-- some (some "WORLD")

-- same wire, three times slower, speed not disclosed:
#eval (transmitStr "HELLO WORLD").map fun sig =>
  (decodeAdaptive (scale 3 sig)).map msgToStr
-- some (some "HELLO WORLD")

What's not covered

So the model is: per-run additive jitter at known speed, or per-run multiplicative band at unknown speed, over an intact run structure. Not covered: corrupted run structure (dropped, split, or merged runs), additive and multiplicative error composed, cumulative clock drift within a message, amplitude noise, or anything probabilistic. Real CW receivers also re-estimate speed continuously; the trailing-anchor estimator here does it once. These are model boundaries, not small print.

Two tricks I'd reuse

• All the stream-parsing lemmas are stated with a continuation: group (classify (timeLetter l g ++ s)) = ... for arbitrary s. The inductions never have to look inside the tail. Without this the word-level induction gets ugly fast.
• The upper layers only touch durations through the classifier lemmas. Additive robustness was: upgrade two lemmas from points to radius-1 balls, change nothing else. Speed robustness was: same two lemmas again, ratio balls this time. If you set up the layering right, each new theorem costs one new bridge.

Also, a Lean gotcha for the search engines: ∃ e g, p = (e.dur, g.dur) with unannotated binders doesn't just fail to infer the field notation — it can send the elaborator into a whnf timeout. Write ∃ (e : Element) (g : Gap), ....

Maybe later

• Compose the two error models (multiplicative band + additive jitter).
• Probabilistic noise and error rates — a different project's worth of Mathlib probability.
• The information-theory roof — unique decodability, Kraft–McMillan — which Mathlib doesn't have yet. Morse would be the fun witness (uniquely decodable, not prefix-free) rather than the point.

Build

lake exe cache get && lake build

Lean v4.31.0, Mathlib pinned in lakefile.toml.