totalRecoveryCost_pos

formal source

  56    totalRecoveryCost (n + 1) = totalRecoveryCost n + perBitCost := by
  57  unfold totalRecoveryCost; push_cast; ring
  58
  59theorem totalRecoveryCost_pos {n : ℕ} (h : 1 ≤ n) : 0 < totalRecoveryCost n := by
  60  unfold totalRecoveryCost
  61  exact mul_pos (by exact_mod_cast (by omega : 0 < n)) perBitCost_pos
  62
  63/-- Total cost is strictly monotonic in key size. -/
  64theorem totalRecoveryCost_strict_mono {n m : ℕ} (h : n < m) :
  65    totalRecoveryCost n < totalRecoveryCost m := by
  66  unfold totalRecoveryCost
  67  have h_real : (n : ℝ) < (m : ℝ) := by exact_mod_cast h
  68  exact (mul_lt_mul_iff_of_pos_right perBitCost_pos).mpr h_real
  69
  70/-! ## §3. Doubling-key-size cost identity -/
  71
  72/-- Doubling the key size doubles the recovery cost. -/
  73theorem totalRecoveryCost_double (n : ℕ) :
  74    totalRecoveryCost (2 * n) = 2 * totalRecoveryCost n := by
  75  unfold totalRecoveryCost
  76  push_cast
  77  ring
  78
  79/-! ## §4. Master certificate -/
  80
  81structure RSCryptographicBoundCert where
  82  perBit_pos : 0 < perBitCost
  83  total_zero : totalRecoveryCost 0 = 0
  84  total_succ : ∀ n, totalRecoveryCost (n + 1) = totalRecoveryCost n + perBitCost
  85  total_pos : ∀ {n : ℕ}, 1 ≤ n → 0 < totalRecoveryCost n
  86  total_strict_mono : ∀ {n m : ℕ}, n < m → totalRecoveryCost n < totalRecoveryCost m
  87  total_double : ∀ n, totalRecoveryCost (2 * n) = 2 * totalRecoveryCost n
  88
  89def rSCryptographicBoundCert : RSCryptographicBoundCert where