Repackage all finite joint flow orders into the spatial smoothness witness required by the consumed App. B.2 inverse-flow data.

theorem AVenhance.Infra.Construction.constructionFlowInv_spatial_smooth_of_joint_orders {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hjoint : ∀ (m n : ℕ), ContDiff ℝ ↑n fun (p : ℝ × Homogenization.Vec 2 × ℝ) => constructionFlow hseq m p.1 p.2.1 p.2.2) (m : ℕ) (s u : ℝ) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => constructionFlowInv hseq m (s + u) x s

theorem AVenhance.Infra.Construction.AppB2Smoothness.identity_orderedPartial_one (x : Homogenization.Vec 2) (I : Fin 1 → Fin 2) : FaaDiBruno.orderedPartial 1 (fun (y : Homogenization.Vec 2) => y) x I = FaaDiBruno.coordinateVector 2 (I 0)

theorem AVenhance.Infra.Construction.AppB2Smoothness.identity_orderedPartial_ge_two (x : Homogenization.Vec 2) {n : ℕ} (hn : 2 ≤ n) (I : Fin n → Fin 2) : FaaDiBruno.orderedPartial n (fun (y : Homogenization.Vec 2) => y) x I = 0

theorem AVenhance.Infra.Construction.AppB2Smoothness.identity_derivativeSup_le_one {n : ℕ} (hn : 1 ≤ n) : (FaaDiBruno.derivativeSup n fun (x : Homogenization.Vec 2) => x) ≤ ENNReal.ofReal 1

theorem AVenhance.Infra.Construction.AppB2Smoothness.identity_snorm_le_four_div {n : ℕ} (hn : 1 ≤ n) {S : ℝ} (hS : 0 < S) : FaaDiBruno.snorm (fun (x : Homogenization.Vec 2) => x) n S ≤ ENNReal.ofReal (4 / S)

theorem AVenhance.Infra.Construction.AppB2Smoothness.derivativeSup_add_le_vec {n : ℕ} (f g : Homogenization.Vec 2 → Homogenization.Vec 2) (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) : (FaaDiBruno.derivativeSup n fun (x : Homogenization.Vec 2) => f x + g x) ≤ FaaDiBruno.derivativeSup n f + FaaDiBruno.derivativeSup n g

theorem AVenhance.Infra.Construction.AppB2Smoothness.snorm_add_le_vec {n : ℕ} {S : ℝ} (f g : Homogenization.Vec 2 → Homogenization.Vec 2) (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) : FaaDiBruno.snorm (fun (x : Homogenization.Vec 2) => f x + g x) n S ≤ FaaDiBruno.snorm f n S + FaaDiBruno.snorm g n S

theorem AVenhance.Infra.Construction.AppB2Smoothness.snorm_neg_eq_vec {n : ℕ} {S : ℝ} (f : Homogenization.Vec 2 → Homogenization.Vec 2) : FaaDiBruno.snorm (fun (x : Homogenization.Vec 2) => -f x) n S = FaaDiBruno.snorm f n S

theorem AVenhance.Infra.Construction.AppB2Smoothness.constructionFlow_jointSmooth_of_joint_orders {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (hjoint : ∀ (m n : ℕ), ContDiff ℝ ↑n fun (p : ℝ × Homogenization.Vec 2 × ℝ) => constructionFlow hseq m p.1 p.2.1 p.2.2) : ContDiff ℝ ↑⊤ fun (p : (ℝ × Homogenization.Vec 2) × ℝ) => constructionFlow hseq m p.1.1 p.1.2 p.2

theorem AVenhance.Infra.Construction.AppB2Smoothness.constructionFlow_shift_isFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s : ℝ) : IsFlow (fun (t : ℝ) (x : Homogenization.Vec 2) => b (s + t) x) fun (t : ℝ) (x : Homogenization.Vec 2) (r : ℝ) => X (s + t) x (s + r)

theorem AVenhance.Infra.Construction.AppB2Smoothness.constructionFlowInv_displacement_data_of_joint_orders {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) {R M : ℕ → ℝ} (hscales : Section2Scales I R M) (hjoint : ∀ (m n : ℕ), ContDiff ℝ ↑n fun (p : ℝ × Homogenization.Vec 2 × ℝ) => constructionFlow hseq m p.1 p.2.1 p.2.2) (m : ℕ) (hprev : Section2StreamInductionHypothesis R M (m - 1)) (s u : ℝ) (hu : |u| ≤ 2 ^ (-6) * (M (m - 1))⁻¹) (n : ℕ) (hn : 1 ≤ n) : (ContDiff ℝ ↑n fun (x : Homogenization.Vec 2) => constructionFlow hseq (m - 1) s x (s + u) - x) ∧ FaaDiBruno.snorm (fun (x : Homogenization.Vec 2) => constructionFlow hseq (m - 1) s x (s + u) - x) n (9 / 8 * R (m - 1)) ≤ ENNReal.ofReal (1 / (4 * R (m - 1)))

theorem AVenhance.Infra.Construction.AppB2Smoothness.constructionFlowInv_snorm_bound_of_joint_orders {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) {R M : ℕ → ℝ} (hscales : Section2Scales I R M) (hjoint : ∀ (m n : ℕ), ContDiff ℝ ↑n fun (p : ℝ × Homogenization.Vec 2 × ℝ) => constructionFlow hseq m p.1 p.2.1 p.2.2) (m : ℕ) (hprev : Section2StreamInductionHypothesis R M (m - 1)) (s u : ℝ) (hu : |u| ≤ 2 ^ (-6) * (M (m - 1))⁻¹) (n : ℕ) (hn : 1 ≤ n) : FaaDiBruno.snorm (fun (x : Homogenization.Vec 2) => constructionFlowInv hseq (m - 1) (s + u) x s) n (9 / 8 * R (m - 1)) ≤ ENNReal.ofReal (5 * (8 / 9) * (R (m - 1))⁻¹)

theorem AVenhance.Infra.Construction.appB2InverseFlowData_of_joint_orders {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) {R M : ℕ → ℝ} (hscales : Section2Scales I R M) (hjoint : ∀ (m n : ℕ), ContDiff ℝ ↑n fun (p : ℝ × Homogenization.Vec 2 × ℝ) => constructionFlow hseq m p.1 p.2.1 p.2.2) : AppB2InverseFlowData I Φ hseq R M

Construct the consumed App. B.2 package from the previous-scale induction bound, provided every finite joint order of the construction flow is available. The finite-order premise assembles the smooth inverse witness; the quantitative field input is exactly e.indyhyp at scale m - 1.

theorem AVenhance.Infra.Construction.appB2InverseFlowData_of_smoothPeriodicFlow {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) {R M : ℕ → ℝ} (hscales : Section2Scales I R M) : AppB2InverseFlowData I Φ hseq R M

Construct all finite joint orders of the construction flow from the merged all-orders ODE theorem. Each scale's stream velocity is a smooth periodic field, and its characterized construction flow is therefore jointly C∞ in target time, initial point, and start time.