Research proof index

Core uniformity lemma: uniform keygen plus unique key per (message, ciphertext) pair implies every (message, ciphertext) conditional has probability (card K)⁻¹. Both Shannon theorems follow from this.

Constructive Shannon direction: if keygen is uniform and each (message, ciphertext) pair is realized by a unique key in support, then perfect secrecy holds. deterministicEnc asserts encryption is deterministic in distribution (singleton support for each fixed (key, message)).

Total-variation distance is convex over a shared bind: if tvDist (f a) (g a) ≤ c for every a ∈ support mx, then tvDist (mx >>= f) (mx >>= g) ≤ c. The real-valued root of the const bound, with ℝ≥0∞ companion ofReal_tvDist_bind_left_le_const.

Under per-family upper bounds on the two U-transform oracle families, decapsulation incurs weighted query cost at most the sum of those bounds.

Under per-family upper bounds on the two U-transform oracle families, encapsulation incurs weighted query cost at most the sum of those bounds.

Index-extraction for Vector.mapM: any component of a vector in the support of the sequenced computation lies in the support of the corresponding component computation.