lambda_0

formal source

  85
  86/-- The bare e-ph coupling at φ-rung 0. Calibrated per material; for
  87H₃S near 1, for LaH₁₀ near 2 (per Drozdov et al. 2019 fits). -/
  88def lambda_0 (lam : ℝ) : ℝ := lam
  89
  90/-- The e-ph coupling at φ-rung `k`: `λ(k) = λ_0 · φ^k`. -/
  91def lambda_at_rung (lam : ℝ) (k : ℕ) : ℝ := lambda_0 lam * Constants.phi ^ k
  92
  93theorem lambda_at_rung_pos {lam : ℝ} (h : 0 < lam) (k : ℕ) :
  94    0 < lambda_at_rung lam k := by
  95  unfold lambda_at_rung lambda_0
  96  exact mul_pos h (pow_pos Constants.phi_pos k)
  97
  98/-- The McMillan exponent at rung `k`: `1.04 (1 + λ_k) / (λ_k − μ*)`,
  99defined for `λ_k > μ*`. -/
 100def mcmillan_exponent (lam : ℝ) (k : ℕ) : ℝ :=
 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 -/