Negligibility of dyadic square-root bounds

An entropy surplus of twice the security parameter gives geometric decay after taking a square root. Polynomially many output rows preserve negligibility. The output and source bit counts need not themselves be polynomially bounded or computable.

Main results

• sqrt_pow_two_div_pow_two_le: the pointwise geometric estimate.
• negligible_mul_sqrt_pow_two_div_pow_two: polynomial losses preserve the estimate, including when the entropy margin holds only eventually.

theorem Cslib.Crypto.sqrt_pow_two_div_pow_two_le {outputBits sourceBits n : ℕ} (hmargin : outputBits + 2 * n ≤ sourceBits) : NNReal.sqrt (2 ^ outputBits / 2 ^ sourceBits) ≤ (1 / 2) ^ n

Twice the security parameter in surplus bits bounds the square-root ratio by 2⁻ⁿ.

theorem Cslib.Crypto.negligible_mul_sqrt_pow_two_div_pow_two {count outputBits sourceBits : ℕ → ℕ} (hcount : PolynomiallyBounded count) (hmargin : ∀ᶠ (n : ℕ) in Filter.atTop, outputBits n + 2 * n ≤ sourceBits n) : Negligible fun (n : ℕ) => ↑(count n) * NNReal.sqrt (2 ^ outputBits n / 2 ^ sourceBits n)

A polynomial number of square-root dyadic errors is negligible under an eventual entropy surplus of twice the security parameter.