Derive every single-step numerical condition from the initial threshold.

theorem KamProject.Arnold1963.Iteration.InitialParameters.angle_loss {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : 10 * ↑(delta δ₁ s) < 2 * ↑(gamma n δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialParameters.action_loss {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : 3 * ↑(beta δ₁ s) < 2 * ↑(delta δ₁ s)

theorem KamProject.Arnold1963.Iteration.InitialParameters.delta_lt_fraction {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : ↑δ₁ < κ

theorem KamProject.Arnold1963.Iteration.InitialParameters.divisor_pos {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : 0 < κ * ↑δ₁

theorem KamProject.Arnold1963.Iteration.InitialParameters.divisor_le_one {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) : κ * ↑δ₁ ≤ 1

theorem KamProject.Arnold1963.Iteration.InitialParameters.delta_sq_lt_divisor {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : ↑(delta δ₁ s) ^ 2 < κ * ↑δ₁

theorem KamProject.Arnold1963.Iteration.InitialParameters.divisor_margin {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : 2 * ↑(beta δ₁ s) < κ * ↑δ₁

theorem KamProject.Arnold1963.Iteration.InitialParameters.perturbation_small {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : perturbation n δ₁ s < ↑(delta δ₁ s) ^ stepExponent n * (κ * ↑δ₁) * ↑(beta δ₁ s) ^ 2

theorem KamProject.Arnold1963.Iteration.InitialParameters.parameters {n : ℕ} {δ₁ θ₀ Θ₀ ρ₀ : NNReal} {κ D : ℝ} (b : InitialParameters n δ₁ θ₀ Θ₀ ρ₀ κ D) (s : ℕ) : IterationParameters n (width n ρ₀ δ₁ s) (beta δ₁ s) (delta δ₁ s) (gamma n δ₁ s) (lower θ₀ δ₁ s) (upper Θ₀ δ₁ s) (κ * ↑δ₁) (perturbation n δ₁ s)