contract 8: the enhancement product bound, including the terminal step. Constants are selected before the ingredients; no temperature datum occurs.

theorem AVenhance.Infra.Section5.RelativeError.KappaProduct.epsilon_delta_le_inverse {β R : ℝ} (I : Ingredients β) (hR : 1 ≤ R) (hΛ : R ^ (delta β)⁻¹ ≤ ↑I.Λ) {j : ℕ} (hj : 1 ≤ j) : epsilon β I.Λ j ^ delta β ≤ R⁻¹

theorem AVenhance.Infra.Section5.RelativeError.KappaProduct.averaging_small_of_inverse {L P e : ℝ} (hL : 0 ≤ L) (hP : 0 ≤ P) (he : 0 ≤ e) (hsmall : e ≤ (1 + 160 / 9 * L * (P + 1))⁻¹) : L * (P * e ^ 2 + e) ≤ 9 / 160