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
proof body
Term-mode proof.
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`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.