totalRecoveryCost_double

formal source

  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
  90  perBit_pos := perBitCost_pos
  91  total_zero := totalRecoveryCost_zero
  92  total_succ := totalRecoveryCost_succ
  93  total_pos := @totalRecoveryCost_pos
  94  total_strict_mono := @totalRecoveryCost_strict_mono
  95  total_double := totalRecoveryCost_double
  96
  97/-- **CRYPTOGRAPHY ONE-STATEMENT.** Per-bit J-cost = `log φ > 0`; total
  98recovery cost is additive over bits; doubling key size exactly doubles
  99recovery cost. -/
 100theorem cryptography_one_statement :
 101    0 < perBitCost ∧
 102    (∀ n, totalRecoveryCost (n + 1) = totalRecoveryCost n + perBitCost) ∧
 103    (∀ n, totalRecoveryCost (2 * n) = 2 * totalRecoveryCost n) :=