phi_golden_recursion

formal source

  85    exact this
  86
  87/-- φ satisfies the golden recursion φ = 1 + 1/φ (structural identity). -/
  88theorem phi_golden_recursion : preferredAspectRatio * (preferredAspectRatio - 1) = 1 := by
  89  unfold preferredAspectRatio
  90  have h : phi ^ 2 = phi + 1 := phi_sq_eq
  91  have hphi : phi ^ 2 = phi * phi := sq phi
  92  rw [hphi] at h
  93  linarith [h]
  94
  95structure GoldenSectionCert where
  96  ratio_gt_one : 1 < preferredAspectRatio
  97  ratio_in_band : (1.4 : ℝ) < preferredAspectRatio ∧ preferredAspectRatio < 1.9
  98  golden_recursion : preferredAspectRatio * (preferredAspectRatio - 1) = 1
  99  cost_at_ideal : ∀ r : ℝ, r ≠ 0 → proportionCost r r = 0
 100  cost_nonneg : ∀ a i : ℝ, 0 < a → 0 < i → 0 ≤ proportionCost a i
 101
 102noncomputable def cert : GoldenSectionCert where
 103  ratio_gt_one := preferredAspectRatio_gt_one
 104  ratio_in_band := preferredAspectRatio_in_aesthetic_band
 105  golden_recursion := phi_golden_recursion
 106  cost_at_ideal := proportionCost_at_ideal
 107  cost_nonneg := proportionCost_nonneg
 108
 109theorem cert_inhabited : Nonempty GoldenSectionCert := ⟨cert⟩
 110
 111end
 112end GoldenSectionInProportion
 113end Architecture
 114end IndisputableMonolith