resonance_increases_stability

formal source

  65
  66/-- **THEOREM: Coherence Increases System Stability**
  67    Using resonant scales increases the overall stability of the biological system. -/
  68theorem resonance_increases_stability (r_init r_resonant : ℝ) (hr_init : r_init > 0) (hr_res : r_resonant > 0) :
  69    ¬ ResonantScale r_init →
  70    ResonantScale r_resonant →
  71    SystemStability r_init < SystemStability r_resonant := by
  72  intro h_non_res h_res
  73  -- 1. Resonant stability is 1
  74  have h_res_strain := resonant_minimization r_resonant hr_res h_res
  75  unfold SystemStability
  76  rw [h_res_strain]
  77  simp only [add_zero, div_one]
  78  -- 2. Non-resonant stability is < 1
  79  unfold GeometricStrain
  80  simp only [hr_init, ↓reduceDIte]
  81  let n := Int.floor (Real.log r_init / Real.log phi + 1 / 2)
  82  have h_ratio_ne_one : r_init / (phi ^ (n : ℝ)) ≠ 1 := by
  83    intro h_eq
  84    have h_r_init : r_init = phi ^ (n : ℝ) := by
  85      have h_pow_pos := Real.rpow_pos_of_pos phi_pos (n : ℝ)
  86      rw [div_eq_one_iff_eq h_pow_pos.ne'] at h_eq
  87      exact h_eq
  88    exact h_non_res ⟨n, h_r_init⟩
  89  have h_ratio_pos : 0 < r_init / (phi ^ (n : ℝ)) := by
  90    apply div_pos hr_init
  91    exact Real.rpow_pos_of_pos phi_pos _
  92  have h_pos : 0 < Jcost (r_init / (phi ^ (n : ℝ))) := by
  93    apply Jcost_pos_of_ne_one
  94    · exact h_ratio_pos
  95    · exact h_ratio_ne_one
  96  -- 1 / (1 + h_pos) < 1
  97  have h_denom : 1 < 1 + Jcost (r_init / (phi ^ (n : ℝ))) := by
  98    linarith