`phi_harmonic_forced`

definition

show as: view math explainer →

module: IndisputableMonolith.Cost.FrequencyLadder
domain: Cost
line: 92 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost.FrequencyLadder on GitHub at line 92.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.