Flow-slice identification and time window on supp ξ_{m,k}

Shared basics for the analytic inputs of the centered ergodic estimates: the actual flow slices are the Section 2 flows started at s = l_k τ''_m run for time t - s, the time t - s lies in the Section 2 window, and the window gives the sharp smallness 2^23 |t - s| a_{m-1} ≤ ε_{m-1}^{2δ}/4.

theorem AVenhance.Infra.Section5.Contracts.sdw_xFlow_slice_eq {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : (fun (y : Homogenization.Vec 2) => I.xFlow hΦ m l t y) = fun (y : Homogenization.Vec 2) => constructionFlow hΦ (m - 1) (↑l * tauPP β I.Λ m + (t - ↑l * tauPP β I.Λ m)) y (↑l * tauPP β I.Λ m)

theorem AVenhance.Infra.Section5.Contracts.sdw_xFlowInv_slice_eq {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : (fun (y : Homogenization.Vec 2) => I.xFlowInv hΦ m l t y) = fun (y : Homogenization.Vec 2) => constructionFlowInv hΦ (m - 1) (↑l * tauPP β I.Λ m + (t - ↑l * tauPP β I.Λ m)) y (↑l * tauPP β I.Λ m)

theorem AVenhance.Infra.Section5.Contracts.sdw_scale_arith {e b x d : ℝ} (he : 0 < e) (hx : x ≤ 2 ^ (-25) * e ^ (2 - b + 2 * d)) : 2 ^ 23 * x * e ^ (b - 2) ≤ e ^ (2 * d) / 4

Abstract-real scale arithmetic: if x ≤ 2^{-25} e^{2-b+2δ} then 2^23 x e^{b-2} ≤ e^{2δ}/4.

theorem AVenhance.Infra.Section5.Contracts.sdw_scale_window {e b x d : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hd : 0 ≤ d) (hx : x ≤ 2 ^ (-25) * e ^ (2 - b + 2 * d)) : x ≤ 2 ^ (-25) * (e ^ (b - 2))⁻¹

Abstract-real scale arithmetic: 2^{-25} e^{2-b+2δ} ≤ 2^{-25} (e^{b-2})⁻¹ for e ≤ 1, 0 ≤ δ.

theorem AVenhance.Infra.Section5.Contracts.sdw_eps_pos {β : ℝ} (I : Ingredients β) (n : ℕ) : 0 < epsilon β I.Λ n

theorem AVenhance.Infra.Section5.Contracts.sdw_eps_le_one {β : ℝ} (I : Ingredients β) (n : ℕ) : epsilon β I.Λ n ≤ 1

theorem AVenhance.Infra.Section5.Contracts.sdw_flow_window_scale {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) : |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| ≤ 2 ^ (-25) * (a β I.Λ (m - 1))⁻¹ ∧ 2 ^ 23 * |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| * a β I.Λ (m - 1) ≤ epsilon β I.Λ (m - 1) ^ (2 * delta β) / 4

Flow-time window and the resulting smallness 2^23 |t - l_kτ''| a_{m-1} ≤ ε_{m-1}^{2δ}/4.