The active refresh flow starts at time zero.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_active_index {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (hk : I.xiMK m k 0 ≠ 0) : k ∈ Finset.Icc (-1) 1

Only indices -1, 0 and 1 can be active initially.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_cutoff_sum {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : ∑ k ∈ ⋯.toFinset, |I.xiMK m k 0| ≤ 3

Uniform finite cutoff budget for the actual initial corrector sum.

theorem AVenhance.Infra.Section5.RelativeError.relative_hatZeta_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : I.hatZetaML m 0 0 = 1

Zero lies in the core of refresh cutoff zero.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_active_lIdx {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (hk : I.xiMK m k 0 ≠ 0) : lIdx β I.Λ m k = 0

Every initial active small cutoff is assigned to refresh cell zero.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_active_xFlow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (hk : I.xiMK m k 0 ≠ 0) : I.xFlow hΦ m (lIdx β I.Λ m k) 0 = id

The active initial flow is exactly the identity, without a flow-size premise.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_active_flowGrad_le_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (hk : I.xiMK m k 0 ≠ 0) (x : Homogenization.Vec 2) (i j : Fin 2) : |I.flowGrad hΦ m (lIdx β I.Λ m k) 0 x i j| ≤ 2

Discharged active-flow entry bound for the corrector estimate.