theorem calculation_1 {a : ℕ} (s : ℤ) : 4 * ↑(defaultD a) ^ (-2) * ↑(defaultD a) ^ (s + 3) = 4 * ↑(defaultD a) ^ (s + 1)

theorem calculation_2 {a : ℕ} (s : ℤ) : 8⁻¹ * ↑(defaultD a) ^ (-3) * ↑(defaultD a) ^ (s + 3) = 8⁻¹ * ↑(defaultD a) ^ s

theorem calculation_10 {a : ℕ} (h : 100 < ↑(defaultD a)) : (100 + 4 * ↑(defaultD a) ^ (-2) + 8⁻¹ * ↑(defaultD a) ^ (-3)) * ↑(defaultD a) ^ (-1) < 2

theorem calculation_3 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {x y : ℤ} (h : x + 3 < y) : 100 * ↑(defaultD a) ^ (x + 3) + 4 * ↑(defaultD a) ^ (-2) * ↑(defaultD a) ^ (x + 3) + 8⁻¹ * ↑(defaultD a) ^ (-3) * ↑(defaultD a) ^ (x + 3) + 8 * ↑(defaultD a) ^ y < 10 * ↑(defaultD a) ^ y

theorem calculation_4 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {s_1 s_2 s_3 : ℤ} {dist_a dist_b dist_c dist_d : ℝ} (lt_1 : dist_a < 100 * ↑(defaultD a) ^ (s_1 + 3)) (lt_2 : dist_b < 8 * ↑(defaultD a) ^ s_3) (lt_3 : dist_c < 8⁻¹ * ↑(defaultD a) ^ s_1) (lt_4 : dist_d < 4 * ↑(defaultD a) ^ s_2) (three : s_1 + 3 < s_3) (plusOne : s_2 = s_1 + 1) : dist_a + dist_d + dist_c + dist_b < 10 * ↑(defaultD a) ^ s_3

theorem calculation_logD_64 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] : Real.logb (↑(defaultD a)) 64 < 1

theorem calculation_5 {a : ℕ} {dist_1 dist_2 : ℝ} (h : dist_1 ≤ (2 ^ ↑a) ^ 6 * dist_2) : 2 ^ (-100 * ↑a) * dist_1 ≤ 2 ^ (-94 * ↑a) * dist_2

theorem calculation_6 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s : ℤ) : ↑(defaultD a) ^ (s + 3) = ↑(defaultD a) ^ (s + 2) * ↑(defaultD a)

theorem calculation_7 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s : ℤ) : 100 * (↑(defaultD a) ^ (s + 2) * ↑(defaultD a)) = ↑(defaultA a) ^ (100 * a) * (100 * ↑(defaultD a) ^ (s + 2))

theorem calculation_8 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {dist_1 dist_2 : ℝ} (h : dist_1 * 2 ^ (100 * ↑a) ≤ dist_2) : dist_1 ≤ 2 ^ (-100 * ↑a) * dist_2

theorem calculation_9 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (h : 1 ≤ 2 ^ (-94 * ↑a)) : False

theorem calculation_11 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s : ℤ) : 100 * ↑(defaultD a) ^ (s + 2) + 4 * ↑(defaultD a) ^ (s + 1) < 128 * ↑(defaultD a) ^ (s + 2)

theorem calculation_12 {a : ℕ} (s : ℝ) : 128 * ↑(defaultD a) ^ (s + 2) = 2 ^ (200 * a ^ 2 + 4) * (8 * ↑(defaultD a) ^ s)

theorem calculation_13 {a : ℕ} : 2 ^ (200 * a ^ 3 + 4 * a) = ↑(defaultA a) ^ (200 * a ^ 2 + 4)

theorem calculation_14 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (n : ℕ) : 2 ^ (↑(defaultZ a) * ↑n / 2 - 201 * ↑a ^ 3) ≤ 2 ^ (↑(defaultZ a) * ↑n / 2 - (200 * ↑a ^ 3 + 4 * ↑a))

theorem calculation_15 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (dist zon : ℝ) (h : 2 ^ zon ≤ 2 ^ (200 * a ^ 3 + 4 * a) * dist) : 2 ^ (zon - (200 * ↑a ^ 3 + 4 * ↑a)) ≤ dist

theorem calculation_16 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] (s : ℤ) : 4 * ↑(defaultD a) ^ s < 100 * ↑(defaultD a) ^ (s + 1)

theorem calculation_7_7_4 {X : Type u_1} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X} [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] {n : ℕ} : 1 ≤ 2 ^ (defaultZ a * (n + 1)) - 4