RSCryptographicBoundCert

formal source

  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) :=
 104  ⟨perBitCost_pos, totalRecoveryCost_succ, totalRecoveryCost_double⟩
 105
 106end
 107
 108end RSCryptographicBound
 109end Cryptography
 110end IndisputableMonolith