proportionCost_nonneg

formal source

  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
  78      unfold Constants.phi
  79      have hsq : Real.sqrt 5 < 2.25 := by
  80        rw [show (2.25 : ℝ) = Real.sqrt (2.25 ^ 2) from by
  81          rw [Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 2.25)]]
  82        apply Real.sqrt_lt_sqrt (by norm_num)
  83        norm_num
  84      linarith
  85    exact this
  86
  87/-- φ satisfies the golden recursion φ = 1 + 1/φ (structural identity). -/