phi_ladder_optimization_collapses

formal source

 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⟩
 135
 136/-! ## §4. Master certificate -/
 137
 138/-- **HYDRIDE SC OPTIMIZATION MASTER CERTIFICATE.** Five clauses:
 139
 1401. `mu_star_in_band`: μ* ∈ (0, 1).
 1412. `lambda_pos`: e-ph coupling positive.
 1423. `T_c_optimization_exists`: optimal rung exists on any finite range.
 1434. `phi_ladder_collapses`: optimization reduces to single integer parameter.
 1445. `phonon_rung_imported`: phonon rung is imported from PhiLadderPhononResonance. -/
 145structure HydrideSCOptimizationCert where
 146  mu_star_in_band : 0 < mu_star ∧ mu_star < 1
 147  lambda_pos : ∀ {lam : ℝ}, 0 < lam → ∀ k, 0 < lambda_at_rung lam k
 148  T_c_optimization_exists : ∀ omega_0 lam (n : ℕ), 0 < n →
 149    ∃ k_opt ∈ Finset.range n,
 150      ∀ k ∈ Finset.range n, T_c_phi_rung omega_0 lam k ≤ T_c_phi_rung omega_0 lam k_opt
 151  phi_ladder_collapses : ∀ omega_0 lam (n : ℕ) (h : 0 < n),
 152    ∃ k_opt : ℕ, k_opt ∈ Finset.range n ∧
 153      T_c_phi_rung omega_0 lam k_opt =
 154        Finset.sup' (Finset.range n)