theorem proved term proof

`securityLevelRatio_gt_one`

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

formal statement (Lean)

  46theorem securityLevelRatio_gt_one : 1 < securityLevelRatio := by

proof body

Term-mode proof.

  47  unfold securityLevelRatio
  48  rw [show (1 : ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm]
  49  exact Real.sqrt_lt_sqrt (by norm_num) one_lt_phi
  50
  51/-- Standard symmetric key lengths (bits). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

cert in IndisputableMonolith.Cryptography.KeyLengthFromPhiLadder decl_use

depends on (5)

Lean names referenced from this declaration's body.

one_lt_phi in IndisputableMonolith.Constants decl_use
securityLevelRatio in IndisputableMonolith.Cryptography.KeyLengthFromPhiLadder decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
one_lt_phi in IndisputableMonolith.PhiSupport decl_use
one_lt_phi in IndisputableMonolith.PhiSupport.Lemmas decl_use