preferredAspectRatio_gt_one

formal source

  44/-- The golden ratio as the aesthetically preferred aspect ratio. -/
  45def preferredAspectRatio : ℝ := phi
  46
  47theorem preferredAspectRatio_gt_one : 1 < preferredAspectRatio := one_lt_phi
  48
  49/-- J-cost on the aspect ratio deviation. -/
  50def proportionCost (actual_ratio ideal_ratio : ℝ) : ℝ :=
  51  Jcost (actual_ratio / ideal_ratio)
  52
  53theorem proportionCost_at_ideal (r : ℝ) (h : r ≠ 0) :
  54    proportionCost r r = 0 := by
  55  unfold proportionCost; rw [div_self h]; exact Jcost_unit0
  56
  57theorem proportionCost_nonneg (a i : ℝ) (ha : 0 < a) (hi : 0 < i) :
  58    0 ≤ proportionCost a i := by
  59  unfold proportionCost; exact Jcost_nonneg (div_pos ha hi)
  60
  61/-- The φ:1 rectangle is in the aesthetic preference band (1.4, 1.9). -/
  62theorem preferredAspectRatio_in_aesthetic_band :
  63    (1.4 : ℝ) < preferredAspectRatio ∧ preferredAspectRatio < 1.9 := by
  64  unfold preferredAspectRatio
  65  constructor
  66  · -- phi = (1 + sqrt 5)/2 > 1.4 since sqrt 5 > 1.8
  67    have : (1.4 : ℝ) < Constants.phi := by
  68      unfold Constants.phi
  69      have hsq : Real.sqrt 5 > 1.8 := by
  70        rw [show (1.8 : ℝ) = Real.sqrt (1.8 ^ 2) from by
  71          rw [Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 1.8)]]
  72        apply Real.sqrt_lt_sqrt (by norm_num)
  73        norm_num
  74      linarith
  75    exact this
  76  · -- phi < 1.9 since sqrt 5 < 2.25 would give phi < 1.625 < 1.9
  77    have : Constants.phi < (1.9 : ℝ) := by