PhiHarmonicForced

formal source

  81    2. Self-similar ratios (r² = r + 1) are the scale-invariant resonances
  82    3. φ is the unique positive self-similar ratio (from T6)
  83    4. Therefore f × φ is the unique first φ-harmonic of f -/
  84structure PhiHarmonicForced (f : ℝ) where
  85  harmonic : ℝ
  86  harmonic_eq : harmonic = f * phi
  87  ratio_is_phi : harmonic / f = phi
  88  ratio_self_similar : IsSelfSimilarRatio (harmonic / f)
  89  ratio_unique : ∀ r > 0, IsSelfSimilarRatio r → r = phi
  90
  91/-- The φ-harmonic is forced for any positive frequency. -/
  92noncomputable def phi_harmonic_forced {f : ℝ} (hf : 0 < f) : PhiHarmonicForced f where
  93  harmonic := f * phi
  94  harmonic_eq := rfl
  95  ratio_is_phi := by rw [mul_div_cancel_left₀ _ (ne_of_gt hf)]
  96  ratio_self_similar := by
  97    rw [mul_div_cancel_left₀ _ (ne_of_gt hf)]
  98    exact phi_is_self_similar
  99  ratio_unique := fun r hr_pos hr_ss => phi_unique_self_similar hr_pos hr_ss
 100
 101end FrequencyLadder
 102end Cost
 103end IndisputableMonolith