feat(Crypto): add negligible bounds for security games

Cslib.lean

@@ -99,6 +99,7 @@ public import Cslib.Computability.URM.Defs
 public import Cslib.Computability.URM.Execution
 public import Cslib.Computability.URM.StandardForm
 public import Cslib.Computability.URM.StraightLine
+public import Cslib.Crypto.Negligible
 public import Cslib.Crypto.Primitives.PRG.Asymptotic
 public import Cslib.Crypto.Primitives.PRG.Basic
 public import Cslib.Crypto.Primitives.PRG.Defs

Cslib/Crypto/Negligible.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Foundations.Data.Nat.PolynomialBound
+public import Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
+
+/-!
+# Negligible functions
+
+Negligible bounds are Mathlib's superpolynomial decay at natural security parameters.
+This module supplies zero, comparison, and polynomial-loss bounds for security games.
+
+The decay bound may depend on the whole algorithm. Security definitions quantify over that
+algorithm before asserting negligibility; this module does not change that quantifier order.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto
+
+/-- An advantage is negligible when it decays faster than every inverse polynomial in the
+security parameter. This is Mathlib's superpolynomial decay, specialized to natural parameters. -/
+abbrev Negligible (ε : ℕ → ℝ) : Prop :=
+  Asymptotics.SuperpolynomialDecay Filter.atTop (fun n : ℕ => (n : ℝ)) ε
+
+/-- The zero advantage is negligible. -/
+@[simp] theorem negligible_zero : Negligible (fun _ => 0) :=
+  Asymptotics.superpolynomialDecay_zero _ _
+
+/-- A pointwise smaller nonnegative advantage is negligible. -/
+theorem negligible_of_le {ε δ : ℕ → ℝ} (hδ : Negligible δ)
+    (hε : ∀ n, 0 ≤ ε n) (hle : ∀ n, ε n ≤ δ n) : Negligible ε :=
+  hδ.trans_abs_le fun n => abs_le_abs_of_nonneg (hε n) (hle n)
+
+/-- Polynomially bounded factors preserve negligible decay, including for signed functions. -/
+theorem Negligible.polynomiallyBounded_mul {ε : ℕ → ℝ} {p : ℕ → ℕ}
+    (hε : Negligible ε) (hp : PolynomiallyBounded p) :
+    Negligible (fun n => (p n : ℝ) * ε n) := by
+  obtain ⟨d, hd⟩ := hp
+  apply (hε.param_pow_mul d).trans_eventually_abs_le
+  filter_upwards [hd] with n hn
+  simp only [Function.comp_apply, Pi.mul_apply, Pi.pow_apply, abs_mul, abs_pow, Nat.abs_cast]
+  exact mul_le_mul_of_nonneg_right (by exact_mod_cast hn) (abs_nonneg _)
+
+end Cslib.Crypto

Cslib/Crypto/README.md

@@ -19,6 +19,11 @@ The aim is to build end-to-end models where cryptographic operations appear insi
 
 To this end, we expect to leverage the combination of `Crypto` and [Languages](../Languages) to define and formally reason about security protocols. CSLib's common semantics APIs connecting [Languages](../Languages) and [Logics](../Logics) should enable such reasoning.
 
+## Security games
+
+[`Negligible`](Negligible.lean) specializes Mathlib's `SuperpolynomialDecay` to natural security
+parameters, with zero, comparison, and polynomial-loss bounds.
+
 ## Pseudorandom generators
 
 [`Primitives/PRG`](Primitives/PRG) formalizes Boneh and Shoup's Attack Game 3.1 using