T_c_phi_rung

formal source

 101  1.04 * (1 + lambda_at_rung lam k) / (lambda_at_rung lam k - mu_star)
 102
 103/-- The T_c prediction at φ-rung `k` (in K, with `ω_0` in Hz). -/
 104def T_c_phi_rung (omega_0 lam : ℝ) (k : ℕ) : ℝ :=
 105  phonon_rung omega_0 k / 1.2 * Real.exp (-(mcmillan_exponent lam k))
 106
 107/-! ## §2. Existence of optimal rung -/
 108
 109/-- **THEOREM.** On any finite candidate range, an optimal rung
 110exists. This is the single-parameter optimization claim of RS_PAT_010. -/
 111theorem T_c_optimization_finite_search
 112    (omega_0 lam : ℝ) (n : ℕ) (h : 0 < n) :
 113    ∃ k_opt ∈ Finset.range n,
 114      ∀ k ∈ Finset.range n, T_c_phi_rung omega_0 lam k ≤ T_c_phi_rung omega_0 lam k_opt := by
 115  have hne : (Finset.range n).Nonempty := ⟨0, by simp [Finset.mem_range]; exact h⟩
 116  exact Finset.exists_max_image (Finset.range n) (T_c_phi_rung omega_0 lam) hne
 117
 118/-! ## §3. Single-parameter collapse -/
 119
 120/-- **THEOREM.** The optimization landscape collapses from
 121multi-parameter to a single integer parameter (the φ-rung): the
 122optimal T_c on a finite rung range is achieved at exactly one integer
 123`k_opt`. -/
 124theorem phi_ladder_optimization_collapses
 125    (omega_0 lam : ℝ) (n : ℕ) (h : 0 < n) :
 126    ∃ k_opt : ℕ, k_opt ∈ Finset.range n ∧
 127      T_c_phi_rung omega_0 lam k_opt =
 128        Finset.sup' (Finset.range n)
 129          ⟨0, by simp [Finset.mem_range]; exact h⟩
 130          (T_c_phi_rung omega_0 lam) := by
 131  have hne : (Finset.range n).Nonempty := ⟨0, by simp [Finset.mem_range]; exact h⟩
 132  obtain ⟨k_opt, hmem, h_eq⟩ :=
 133    Finset.exists_mem_eq_sup' hne (T_c_phi_rung omega_0 lam)
 134  exact ⟨k_opt, hmem, h_eq.symm⟩