theorem
proved
tactic proof
resonance_increases_stability
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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
99 have h_denom_pos : 0 < 1 + Jcost (r_init / (phi ^ (n : ℝ))) := by
100 linarith
101 apply (div_lt_one h_denom_pos).mpr
102 exact h_denom
103
104/-- **DEFINITION: Octave Loop**
105 A closed recognition sequence of exactly 8 steps. -/