Hoare/Divergence.lean

View source on GitHub

nonExpanding_iff_threshold_triple

A kernel is non-expanding if and only if it preserves every threshold triple: for all n, {measure ≤ n} f {measure ≤ n}. A kernel that does not increase information preserves every upper bound on information — and conversely.

theorem nonExpanding_iff_threshold_triple [Monad M] [Support M]
    {f : Kernel M α β} {mα : InfoMeasure α} {mβ : InfoMeasure β} :
    NonExpanding f mα mβ ↔
      ∀ n : Nat, Triple
        (fun a => mα.measure a ≤ n)
        f
        (fun b => mβ.measure b ≤ n)

Forward direction: if the kernel is non-expanding, then for any input with measure ≤ n, every output has measure ≤ measure(input) ≤ n. Backward direction: pick n = measure(a), and the threshold triple gives measure(b) ≤ measure(a).

This connects to Sato-Katsumata (2023): divergences on a monad give a metric on morphism spaces. NonExpanding is the zero-divergence case. Stating it as a family of Hoare triples connects the metric view to the program logic view. The file notes this is an analogy in spirit, not a formal instance of their relational framework.

Connections

• Hoare/Core.lean — imported; the threshold triples are standard Hoare triples
• Handshake.lean — NonExpanding is defined there; this file gives the triple characterization
• Hoare/Graded.lean — graded triples are a richer quantitative view (cost bound per kernel, not just thresholds)