hydrideSCOptimizationCert

formal source

 157  phonon_rung_imported : ∀ omega_0 k,
 158    phonon_rung omega_0 k = omega_0 * Constants.phi ^ k
 159
 160def hydrideSCOptimizationCert : HydrideSCOptimizationCert where
 161  mu_star_in_band := ⟨mu_star_pos, mu_star_lt_one⟩
 162  lambda_pos := @lambda_at_rung_pos
 163  T_c_optimization_exists := T_c_optimization_finite_search
 164  phi_ladder_collapses := phi_ladder_optimization_collapses
 165  phonon_rung_imported := fun _ _ => rfl
 166
 167/-! ## §5. One-statement summary -/
 168
 169/-- **HYDRIDE SC OPTIMIZATION ONE-STATEMENT.** Three structural facts:
 170
 171(1) The phonon rung is `ω_0 · φ^k`, derived from
 172    `Materials.PhiLadderPhononResonance` (not asserted).
 173(2) The Coulomb pseudopotential `μ* = 0.1` is in the standard Eliashberg
 174    band `(0, 1)`.
 175(3) The hydride superconductor T_c optimization on any finite φ-rung
 176    range reduces to a single-parameter integer search (the structural
 177    content of RS_PAT_010). -/
 178theorem hydride_sc_optimization_one_statement
 179    (omega_0 lam : ℝ) (n : ℕ) (hn : 0 < n) :
 180    (∀ k, phonon_rung omega_0 k = omega_0 * Constants.phi ^ k) ∧
 181    (0 < mu_star ∧ mu_star < 1) ∧
 182    (∃ k_opt ∈ Finset.range n,
 183      ∀ k ∈ Finset.range n, T_c_phi_rung omega_0 lam k ≤ T_c_phi_rung omega_0 lam k_opt) :=
 184  ⟨fun _ => rfl, ⟨mu_star_pos, mu_star_lt_one⟩,
 185   T_c_optimization_finite_search omega_0 lam n hn⟩
 186
 187end
 188
 189end HydrideSCOptimization
 190end Materials