Scalar absorption of the positive half-cell source estimate. All amplitude parameters are nonnegative; the zero-amplitude case is included.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_source_time_absorb {b ν L C K E S : ℝ} (hb : 0 ≤ b) (hν : 0 ≤ ν) (hL : 0 ≤ L) (hC : 0 ≤ C) (hK : 0 ≤ K) (hE : 0 ≤ E) (hS : 0 ≤ S) (hscale : b * ν * L ^ 2 ≤ K * E ^ 2) : 2 * √b * (C * √ν * L * S) ≤ 2 * C * √K * E * S

Square-root time absorption at an abstract relative amplitude.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_diffusivity_rate_cancel {e γ ν C a : ℝ} (he : 0 < e) (hν : ν ≤ C * (a * e ^ (2 + γ))) : ν * (e ^ (-(1 + γ / 2))) ^ 2 ≤ C * a

The temperature spatial rate cancels the previous-scale diffusivity power exactly; no estimate of the temperature itself is involved.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_half_cell_lt_one {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : tauPP β I.Λ m / 2 < 1

The first half-cell lies strictly inside the unit time interval.