Quantitative control of the pulled-flow Jacobians on the supports of the transition cutoffs.

theorem AVenhance.Infra.Section5.R46FluxFlow.tauCellFactor_ge_five {β : ℝ} (I : Ingredients β) (m : ℕ) (_hm : 1 ≤ m) : 5 ≤ Ingredients.tauCellFactor β I.Λ m

theorem AVenhance.Infra.Section5.R46FluxFlow.tau_le_tauPP_quarter {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) : tau β I.Λ m ≤ tauPP β I.Λ m / 25

theorem AVenhance.Infra.Section5.R46FluxFlow.tauP_le_tauPP_fifth {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) : tauP β I.Λ m ≤ tauPP β I.Λ m / 5

theorem AVenhance.Infra.Section5.hatXiML_time_distance_le_tauPP {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (hne : I.hatXiML m l t ≠ 0) : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m

A nonzero translated hatXi coefficient is supported within one large cell of its flow's initial time.

theorem AVenhance.Infra.Section5.lIdx_flow_time_distance_le_tauPP {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (k : ℤ) (t : ℝ) (hξ : I.xiMK m k t ≠ 0) : |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| ≤ tauPP β I.Λ m

The flow assigned to an active small cutoff also starts within one large cell of the target time.

theorem AVenhance.Infra.Section5.R46FluxFlow.tauPP_le_inverse_amplitude_rpow {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) : tauPP β I.Λ m ≤ 2 ^ (-25) * (a β I.Λ (m - 1))⁻¹ * epsilon β I.Λ (m - 1) ^ (2 * delta β)

theorem AVenhance.Infra.Section5.flowGrad_entry_close_on_tauPP_window {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (Cmat : ℝ) (hseq : IsStreamSeq I Φ) (hflow : FlowBoundsData I Φ hseq Cmat) (m : ℕ) (hm : 2 ≤ m) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (ht : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m) (i j : Fin 2) : |(I.flowGrad hseq m l t x - 1) i j| ≤ 1 / 4 * epsilon β I.Λ (m - 1) ^ (2 * delta β)

Componentwise flow-Jacobian distortion from the actual stream-function estimates flow_close field. The stronger epsilon^(2δ) factor comes from the exact time scale.