def definition def or abbrev

`cert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  64noncomputable def cert : KeyLengthCert where
  65  ratio_pos := securityLevelRatio_pos

Definition body.

  66  ratio_gt_one := securityLevelRatio_gt_one
  67  key_doubling := keyLength_doubling
  68

Lean names referenced from this declaration's body.

KeyLengthCert in IndisputableMonolith.Cryptography.KeyLengthFromPhiLadder decl_use
keyLength_doubling in IndisputableMonolith.Cryptography.KeyLengthFromPhiLadder decl_use
securityLevelRatio_gt_one in IndisputableMonolith.Cryptography.KeyLengthFromPhiLadder decl_use
securityLevelRatio_pos in IndisputableMonolith.Cryptography.KeyLengthFromPhiLadder decl_use