phi_cost_fixed_point

formal source

  66
  67/-- φ is the cost fixed point: φ = 1 + 1/φ.
  68    Follows directly from φ² = φ + 1. -/
  69theorem phi_cost_fixed_point : phi = 1 + 1 / phi := by
  70  have hsq := phi_sq_eq
  71  have hne := phi_ne_zero
  72  field_simp at hsq ⊢; linarith
  73
  74/-! ## The φ-Harmonic Theorem -/
  75
  76/-- For any positive frequency f, the first φ-harmonic is f × φ.
  77    This is the minimal-cost non-trivial resonance above f.
  78
  79    The forcing chain:
  80    1. J(r) is the cost of ratio r (from T5)
  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